Wolfram Physics Project - Working Session Tuesday, July 28, 2020 [Metamathematics _ Part 3]

154.979 --> 155.72

Hello everyone .

We are back trying to talk about meta mathematics and its relationship to our physics project .

The surprising unification of uh in a sense , the dynamics of mathematics and the dynamics of the physical world .

And this is uh this is the notebook that Jonathan was using last time um to talk about the in a sense just to summarize and , and um Jonathan should uh interrupt me as appropriate .

But um uh the basic idea is our multi way systems can be thought of the rules .

The underlying rules for the multi way system can be thought of as the uh just as they can be thought of as the operation of the rules of physics .

They can also be uh rules of mathematics that is the application of mathematical um uh um uh Axio systems .

And um the so , so in a sense this is so one interpretation and again , we , we need to get these a little bit straight , one interpretation here is that what we're thinking about is theorems show the equivalence between things .

So for example , these might be two representations , these might be a representation of a word in a group .

And this uh a connection here might say according to the axioms of the group or groups in general , that word is equivalent to this other word .

And therefore there is a theorem that says this is equal to that .

And then there is a progression of sort of what's equal to what that you get by following down these paths .

And a that's kind of , and , and then the idea is to encode a sort of a , a base axiom system as the underlying collection of connections here .

And I had examples of this even in the N K S book of doing things like that .

Then new idea , the the notion is to think about foliation of this uh graph as corresponding to models of the underlying system .

So in other words , we here , we're saying based on the underlying axioms , we can deduce that this uh this turns into this , that this is equal to this and so on .

But now if we add a model which essentially allows us to , which essentially coordinates this picture , this is sort of an arbitrary coordinate system we're using here .

But the coordinator sizes this picture , then we say that that coordinate system says that anything that's below something else in this picture is follows from or is equal to that .

Now , I'm , I'm already a little confused here because as soon as we start thinking about it , I think we had some foliation someplace somewhere here .

Um are we imagining in this picture where these things are terms , are we imagining that we're saying that any time you are essentially going down the orthogonal direction to the foliation , that is a , a , an an equality relation is that um Jonathan or X ?

Is that , is that what we're saying here or , or not ?

Well , I mean , this , this distinction is why I spent so long talking about , you know , clarifying the distinction between the group oid structure and the top structure , right ?

Where , where one is simply localizable and the other one has isomorphism everywhere .

So in the localizable case , it's possible to turn implications into qualities .

But in the group oid case , it's you know that all , all the implications are already equalities .

That's , you know , that that's the clarification .

Sorry , say that again , say that again , the uh for the group oid case , I understand that what we've done is we've turned every one of these into a two way uh into a two way thing .

Right .

Right .

Right .

So , so because um because the sort of fundamental structure that we're dealing with , which is the rule or multi way system has a group structure , you know , but by design , so to speak , um and because every other structure can be viewed as being either a foliation or a vibration of that rule or multi way system , they inherit not a full group oid structure but a topos structure in which it's not the case that every morphism is an isomorphism .

But it's the case that it , that the uh topos can be localized .

So you can , you can convert a subset of morphism into isomorphism .

OK .

I'm not .

OK .

So , so when you say , so generally , these one way arrows are thought of as like the morphism of category theory , a two-way arrow is like an isomorphism .

So when you say um OK , so let , let's just zoom out for a second .

The , the rule limit which I'm claiming is a little bit like some kind of a normalization group fixed point or something .

The rule limit , let's just understand how that arises .

The rule limit comes when you say for every one of these instead of having this particular rule , I'm going to add all possible rules in this case , right ?

It's , you could think of it .

Could you think of it as some kind of completion limit or can you ?

No , that's exactly what it is , right ?

That's the , that's the point .

It's , it's the , as each completion is applying a homotopia and the rule or multi way system is what you obtain in the limit as you add progressively higher order homotopia .

OK .

Let's walk through that for one second .

OK .

So each , each um um uh what we're saying here , a homo , a homotopia is to say we're gonna take that diamond and we're going to crush it , right ?

That's saying that's what a completion would do .

Am I right ?

Uh Yeah .

So there , there would be a homo for parts of length too , right ?

Um uh You know , push shacks on our live stream is asking about this foliation .

This is just a toy example .

But what we're showing here is just a toy example .

This is not a um this is not the , the real thing is much wilder than this .

I have some actual examples in my , in my bulletin .

OK .

Should we , should we look at them ?

Should we ?

Um uh Yeah , if , if , if you'd like it's OK , let's do it , let's do it , let's do it .

Uh Sorry .

Alicia .

OK .

Let me know if anything is invisible .

But um OK , so uh yeah , OK .

So this is the , this is the thing I was saying about completion limits , right ?

So this is an explicit homo between paths here , right ?

Which is , which is represent as a critical pair of completion between every pair of points here , right ?

So , so that OK , hold on , let , let's just walk slowly through this .

So this is saying we're taking , we've got a completion which on its face would just complete a single branch pair to would , would just reemerge a single branch pair .

But when we add that rule globally in it produces this knitting this , this more global knitting of those paths .

Uh Well , no , not , not quite .

I mean , so , so what's happening is you , you're , you're inducing this , this , this is a , this is a sequence of critical pair completions you're inducing by defining this homo between these parts .

So when , when , when you add those in as completion rules , then you get this structure which has that homo , but it also has other , you know , more global effects .

OK .

OK .

OK .

So I , I was wrong about the level so I could have , what I said we were talking about was right .

What , what you could have done instead of doing the homo between those parts that were of length , whatever they were five or something up there , if you just done the length to homo , you would have um gone .

Uh um then you would have um that you would have , you would have still got a globally knitted thing down below because by adding in that , by implementing that Hoopy , you are as a completion , you're having a global effect on the system .

Yes , but it just , it just wouldn't necessarily have knitted the entire parts of those particular parts .

It would have if you had a single diamond , if you had just a one diamond , then it would be , then it would have knitted that diamond but not necessarily a bigger diamond .

Exactly .

And , and which pairs of points you consider to be related in this homo depends on your foliation , right ?

I mean , so in this case , we're foliating with respect to the initial cosmological rest frame here .

So , so we're , you know , so this point is , is associated at that point , this point is associated to that point .

But if we picked a tipped foliation , it would be different as I'll discuss later .

And so this is this is where the relationship between vibrations , homotopia and foliation starts to become more explicit , vibrations , foliation , homotopia and completions becomes more explicit , right .

So , I mean , the basic point here is you're saying we can actualize a foliation by saying not only do we say all those things in that layer we consider to be simultaneous or something , but let's actually make them uh you know , make them identical by having a completion that brings them all that , that connects them .

Is that right .

Right .

Right .

Exactly .

Exactly .

And as I , I , I have some , I have some examples of that later on but OK , this is some kind of boring category theory stuff .

OK .

This is the thing I was saying about this .

I mean , so if you have an object that's that naturally has a group oid structure like a ruling multi way system does , then uh when you construct vibrations of it , those vibrations inherit a top off structure and that top off structure means that you can locally uh turn morphism into isomorphism without changing the global structure of the system .

OK .

I need to understand that .

But by the way , we have a variety of questions on our live stream which indicate that we probably should just give a little bit more introduction because we dived deep into meta mathematics or something and , and no , into a combination of what the heck is this a combination of type theory , meta mathematics , physics and something else ?

Uh In , do we , by the way , do we have Matthew on the , on the ?

Um , uh Yes , we do .

Who hopefully is able to respond to some of these , some of these questions ?

Um uh OK .

I might be useful .

Um , oh , gosh , ah , this is a bunch of questions but I hope Matthew can , can respond to some of these questions because these are gonna take us let let's just do one more pass through what , what the basic idea is .

OK .

So the basic idea is a mathematical theory is represented by a collection of replacement rules which are implementations of the axioms of the mathematical theory , right ?

So go go through to wherever theory , right .

So group theory here it is represented as replacement , you know , here's like associativity represented as patterned replacement rules , right .

OK .

Right .

So it's a multi way system .

So and , and that , and then the issue is um in that multi way system and and the picture you've got there is of a single proof I , right .

And uh um uh there's a question about termination and live stream , but let's for this single proof .

What we're doing is we're saying find a path from this particular term to this other term to prove that they are equal and that by definition is a , is a , uh you know , it's a , it's a finite size thing .

Well , assuming that , assuming there is a finite path between those things .

OK .

But what we're saying now is we're considering the meta mathematics of all possible proofs .

And for that and , and hopefully , we , I don't know whether you made it yet .

The thing that will actually stub a picture from the uh all from the full multi way system to put the stubs in that correspond to this picture here .

Uh No , I that wasn't relevant to what I was writing , but I can , I can do that well , right .

But I mean , so the the point is that the triangles represent things that are branching off into branchial space .

Basically .

I mean , we , we , we did , we did , we did discuss , I mean , we kinda hang on how that works somewhere .

Uh Not sure in this bulletin , what was it in the post ?

He might want to enable dynamics .

So we don't see as many big boxes .

Um Some it was , there was a discussion of that , right ?

I mean , we , we got close , we didn't quite do it though , right ?

So what we wanted to do there , that picture there , what we wanted to do was to make the stubs because effectively what's happening is and every one of those branch branch points there , what is happening if I'm understanding correctly is that in the full multi way causal graph there should be causal connections to other branches .

Right .

Right .

Right .

So , so each one of these critical pair diamonds is an indication of where this particular proof path is plumbed into a larger collection of proof paths in the overall multi way system .

Right .

But I'd just like to see how that , how that works because I think that's gonna , I mean , I mean , I have some , I , I do have some example like way later on , I do have some examples somewhere of how you , how you peel off individual proof paths from the multi way system and how they correspond to the associated proof graphs and things .

Um but it's , I don't know , it's kind of an obvious correspond .

So that's a , that's the multi way graph m multi way causal graph .

I mean that's a , that's an evolution states graph evolution causal graph rather .

Yes .

Right .

OK .

So now let's see how that peels off so that there so every causal edge becomes a dashed edge where you , you're using a particular construct and the proof of some future substitution lemma and every evolution .

But wait a minute , those , those green things were Big Bang events , right ?

Those are initialization events , those don't come from .

But if you go back to your original picture , I mean , no , no , but that's , that's not true .

OK .

Where do the green things come from ?

The their their axioms that Yes , yes , yes .

But OK .

Those are Big Bang events .

Big Bang events are , are the ones that are the initialization events that produce the initial I was , I was thinking of those .

All right , I see your , your point is what , what you're doing there is you're , they are sort of big bang , they're big bang rule events in the sense that those things are the rules that are going to be applied over and over again .

But here we're indicating their provenance by showing , you know , the green thingy , the green shield or something that then goes into that then feeds into that the the the feeds in saying that that edge , I mean that is defining that that arrow .

There is saying that the dotted line above it .

Sorry , that green thing is really the identification for which rule was applied in the dotted line above .

Correct .

Well , it's specifying which construct the rule came from .

Yes , I understand .

But the rule is the thing , the dotted line that joins one yellow , yellow circle to the next yellow circle .

Yeah .

Right .

But that rule , but this is a little different from what we're normally draw because normally in our normal multi way graph , we do not draw the rules as you know , the only thing we draw as rules coming from somewhere else are the causal edges that connect our events .

So a a more direct the orange thing .

Exactly .

Exactly .

But that's , that's what that was what I was saying .

Right .

So that the solid lines are the evolution edges , the dash lines are the causal edges .

That was the point of these pictures .

OK .

But why isn't there a solid line ?

Why is there ?

No , it's a little odd that there are solid lines coming from the axioms .

Why ?

Because I would have thought that the axiom would have a causal edge .

The axiom is the thing from which the event comes or the other way round the axiom is the thing to which you could apply an event from a substitution lemma .

In the linear case like this , it doesn't matter which way around it is .

I , I know it doesn't matter .

I know it doesn't matter but , but in a , in a but in OK .

But right .

All right , fine .

Right .

But I mean , do you have a more sophisticated example of this that isn't just linear ?

Uh Well , yeah , I mean , that was , that was the point of doing this whole discussion over here .

But I was um what I was going to talk about before that was um yes .

So it's the inheritance of the top off structure from the , from the group structure , right ?

That's OK .

Let me understand that .

So , so the point is that as , as you apply um uh um as you apply the these completions , you apply the sort of full set of completions to implement .

No , I'm sorry .

We , we got off track here because what you were saying was given a particular foliation you can in a sense actualize that foliation by adding completions that give you mappings between the equivalent states made the states that are made equivalent by the foliation .

Yeah .

Correct .

Right .

So as you can see uh here for instance , right , that you know this is a pair of uh pair of terms that are , that are not related by the axios , but one can add an additional relation .

Um And then what what that corresponds to if you then actualize it in terms of model theory is a relation like this , which causes two branches to effectively behave as though they're one branch , right ?

You're , you're , you're taking two branches that would otherwise have been independent in the free object and you're constraining them .

So that now I understand .

But if you go back to your foliation picture , what is I mean normally in a foliation , you're saying there is an equivalence , you're describing all things in a slice as being somehow equivalent .

But here , what we're doing is we're saying things that go that follow from one slice from the next are equivalent .

So I'm a little confused by that .

Well , there are two equivalence relations .

That's the whole point , right ?

There , there's , there's the equivalence relation of mutual independence from the axioms and there's the equivalence relation of the actual part , the actual total order induced by the model .

OK .

Fine .

All right .

So , so the equivalent , there's an equivalence relation just like in space time , there's an equivalence relation of space like separation , right ?

You know , there's the equivalent relation of simultaneity but there's also a , well , there's a , there's a unidirectional relation defined by time like ordering .

That's all we're saying .

OK .

But so , so here , let me just understand because here the time like order is a deduction but you are making , you're , you're turning that into an isomorphism somehow that can go both ways .

Is that true or not ?

Uh Yeah , eventually .

But I mean , for the time being , if , if , if that's um things that we didn't get , we still didn't really discuss the , the group inheritance thing .

It , it , for the time being , we can just treat it as a morphism .

It doesn't matter .

OK ?

But you're saying the completions actualize those morphism basically .

But given a particular foliation , you have a bunch of new morphism induced by the foliation , so to speak , which you can then actualize as completions , right .

Right .

And that's ultimately the statement of the un valence axiom as interpreted in our models , right .

It's the statement of equivalence between foliation vibrations and completions .

Um Say that again , say that again , say that again , I missed something there .

So conditions are equivalent um You might want to hit the save button .

Yeah .

Um OK .

So let me understand that .

So let's go through this .

OK .

So a foliation is a foliation of the , the sort of the raw , the raw symbolic mathematics multi way graph .

That's what you mean by that right .

That's the kind of thing we're doing here .

I mean , I mean , inducing a total order on the partial order induced by proof theory .

OK .

Fine .

OK .

The vibration you're talking about now is a vibration from the limit point group oid infinity group oid .

Is that right ?

Well , it could be any fibrate , it could be a , you know , a fib of any structure , well , explain the vibration in this context here .

So I think I , that's what I was doing , right ?

So , so the the this object has multiple branches , you know , this is a free object that has multiple branches .

Yep .

Uh If we wanted to , we could fibrate it .

So we could only consider a subset of those branches .

Yes AAA as as an individual fiber just like in the , you know , in the case , we , we talked about sort of 22 sessions ago .

And the point is one way you can do that is by defining an equivalence relation between those branches , which is a completion and the choice of which completion you make is determined by your vibration .

And the fact that you can uh that there is effectively an equivalence between um defining a homo toy between paths and defining an identity relation between elements is what the un valent Axium says .

So , so the , the , the , the fact that this is a vibration that this can be induced by completion rules and that uh this , you know , the the set of completion rules that you use is determined by your foliation is what the un Axium ultimately means in these formalism .

So let me understand that again more carefully .

So let's let's let's understand how that corresponds to the computational boundness of observers or not , because that's basically saying what what you're saying is this conflation .

So in space time , for example , there isn't a conflation of things in different places in space , in the same sense , right ?

There might be in quantum mechanics but there isn't in space time , right .

Right .

Because in space time , you're not dealing with multi way systems .

Well , I understand your individual experience is not a multi way system , right ?

So you , you could have a that I mean , OK , this is a sort of alien intelligences type discussion , right ?

You you you could have an an alien intelligence that perceived space time in the same way we perceive quantum mechanics where they were effectively looking at elementary bifurcations in the in the spacetime causal network and defining equivalences between those and they would have a very different view of physics , right .

So their view of physics would have no space right ?

In the first approximation , it would just except that they in the same way as we see weird things that are the consequence of branchial geometry .

They would see weird things that are that consequence of spatial structure .

Let's just walk through that for one second a little bit .

Let's just walk through that for a second .

So imagine that we were take the other case in which we were laid out in branchial space and able to consciously observe different parts of branchial space , which we're not currently we have , you know , we are .

So imagine that , you know , you're describing an intelligence where basically its experience of space is like our experience of branchial space .

It's a single threaded experience .

And so what weird effects would you see ?

Well , the weird effects you would see are mostly because you would say , well , well , actually it's a superposition of all these states because , but which it's actually very analogous , isn't it ?

I mean , it , it's the statement here , the , the um so in a sense , we are , so we happen to exist in a single thread of brachial space and multithreaded in physical space .

And if we were single threaded in physical space , it would be , there would be all these effects that come because we would say , gosh , look , there are these things that are coming , you know , we , we're trying to complete everything down so that it , so that we only need to consider essentially our generational states in space .

And is this OK , what is the claim here that that's so if you , if you had an ob if you had observers who were capable , who were localized in um or who , who were forced to collapse spacelike separations down in space time but could move freely in branchial space .

That analog of causal invariants would be multi way invariants in which you could take multi for each of the possible time like paths through the causal network .

There is an isomorphic multi way system that you would observe .

Yes .

And so therefore , which would , which would justify so , you know , implies justification four , collapsing spacetime uh sorry down to a single time like Puff .

OK .

So let's understand why it is , could we imagine , you know , we sort of have only one path that we are conscious of in branchial space .

Is that obvious ?

It has to be that way .

In other words , imagine that we had , you know , our quantum A I , so to speak , this is a good , this is gonna make a good science fiction plot if nothing else .

Um you know , the quantum A I that maintains multiple threads of consciousness in branchial space , right ?

Just as we can say , you know , somebody could say , what do you mean you have , you know , somebody could say you have completely different civilizations and different star systems .

That's outrageous .

Why aren't they just all , you know , how can you perceive that there are two different civilizations in two different star systems ?

All we perceive is that there's AAA certain thread of time .

Um But what would it mean ?

Um uh let's think so , no invariant causal partial order .

Well , that's , well , that's a yet different thing , right ?

That's an even higher level .

But I mean that no look , this is the whole point .

This is the whole point .

The thing that allows us to get reducibility , the thing that allows us to make sense of the world or of mathematics is the fact that we are modding out by all of that .

How did you get from here to there if you don't do that ?

I don't , I don't disagree .

But what's a why , why is this a why is this the strongest ?

It's the same statement , same statement as what , as what you were just discussing ?

I mean , definite things happening in you mean in either either there's an invariant causal partial order across all branches of the multi way system or there isn't .

If there is , then all branches of the multi way system can be treated as observational equivalent .

And if they're , if there's not , then they can't what you're saying , I see your , your point is now I'm very confused because your point is that there isn't a symmetry here between the , the causal invariance is operating in the multi way space and not in physical space which makes there be a different , it isn't the case .

No , it's not , it's not different because you can define multi way invariants which operates in space time , right ?

Where the induced multi way systems for each time like part or isomorphic , that was my whole point .

And so what I'm trying to say is that an A I who sees multiple branches of the multi way system that are , that are not observational equivalent by definition cannot uh construct a causal invariant representation of the world .

If that's what it means for those branches to be an equivalent , just walk through this one more time .

So what we're saying ?

But like I said , so , so either each branch of the multi way system yields an isomorphic causal network and is you know an in an isomorphic causal partial order relation or it doesn't .

So if it does , then you have causal in variants , there is only one branch of the multi way system up to isomorphism .

And that's to the best of our knowledge .

That's , that's basically , that's subjective reality what we have , right .

So what you're claiming is one where there isn't um where , where you have an A I which can , which can simultaneously perceive multiple in equivalent branches of the multi way system , which by definition therefore means that they can't have an invariant causal partial order .

OK .

OK .

So your point is they must be capable of tracking multiple possible causal histories at the same time .

If the underlying rules of physics are causal invariant , then there's no possibility of a multithreaded quantum A I , that's part of my point .

Yeah .

Right .

So , so that point is , but nevertheless , the analog of that there is a multi threaded physical space .

AI that's OK because there is no similar , you know , notion of causal invariants for space .

That's a feature of branchial space but not a feature of space .

Did that make sense ?

Uh Not to me OK , explain I mean , so go on , sorry .

No , I mean , so the point is I'm trying to understand in what sense the look the multi way graph is formed in you know the extent of the multi way graph it it extends in branchial space .

Yeah , obviously .

And if there is causal invariance , there is a , you know a single , as you say , there is a single essentially , you know up to I you know , there's a there's a single objective history to the multi weight to to what happens in the multi way system .

But if you look at the corresponding thing in space time , yeah , then you get multi way invariants which is this , well , you're , you're saying if you said I'm confused , let let's , you know what I'm saying is really , really simple , right ?

So , so each in the multi way evolution in the evolution causal graph , there are multiple causal networks , multiple spacetime , you know one for each branch within each space time , there are multiple time like paths , right ?

The swapping the space , the spatial and branchial directions yields the the analog of causal invariants which would be multi way invariants , which says if you look at for each time like path , what is the associated causal network for that time ?

Like path ?

What ?

Sorry , what is the associated multi way graph for that time ?

Like path , you could ask all those multi way graphs necessarily isomorphic as cyclic graphs .

In other words , is , is the branchial structure the same .

And that's the direct analog of multi of causal invariants for the multi way system .

So the the the symmetric idea , OK .

So , so your point is if you look at the causal graph in space time , each causal , each path through that causal graph has a there are multiple copies of that path right that exist and different from the .

You can you can look at the induced multi way graphs for each , for each such time like path .

But I think it's not quite , there's a slight difference here .

OK .

So let's just go through this .

So this is , this is saying if you are looking at um if you live in space time , then right now if you look at a particular branch , I mean , the the full thing is the multi way causal graph where you can look at it projected onto space time so that you're going down , you know , so you're looking at the , the causal graph projected onto a particular causal graph associated with a particular multi way slice .

So to speak of space time .

Now what you're saying is you can project the multi way causal graph in in one of two directions .

You can either say that you're going to look at these , you know , you're going to take as you know , I mean , yes , I I , I , I think this is what you're saying .

You can project it either way round , you can either say you've got a um and , and either way round the other direction in it looks like something that has a um uh for which you can ask the question .

Is there a um you know , what does causal invariance mean ?

And does causal variance means not causal invariants ?

In this case , it's , it's multi it's evolution in , you know , multi way evolution graph in variants which might not be true , just like causal invariants might not be true , right ?

But the whole point is you're taking this multi way causal network , you can mod out by one of two possible directions .

And then you can ask whether the other combinatorial structures retain is Yes .

Yes , yes , yes , yes .

So I don't see why there's why there's an asymmetry .

Well , in our way of describing no , no , that if if you say you're looking , the main thing is the multi way causal graph , you can project it either in a spatial direction or a branchial direction .

I agree .

OK .

Cool .

Yeah , that's all I said .

But , but I mean , but we have made more claims about causal invariants than about multi way invariants .

We don't think , I think that multi way invariance is true whereas we think it is plausible that causal invariance is true .

And what you're saying is even if you know you , you have made the claim that even if causal invariance isn't true , we'll make it true by doing completions as a result of the way we observe things .

And you're saying just like if we were so , I'm just trying to walk through what it means because we have a better understanding of spatial , you know , a physical space than a branchial space .

If we were these organisms that were essentially doing spatial completions , right ?

What would that look like ?

What would that be doing ?

What that would be saying is it would be like what we do in statistical mechanics , like the coarse graining we do in statistical mechanics .

We'd be saying we're coarse graining across these spatial directions .

Right .

Right .

Right .

And it would be way , it , it would be one , it would be the alternative way of measuring , say um you know , 22 halves of a bell pair or something .

Yes .

OK .

Fair enough .

But I mean , we , what we'd be doing is , you know , what would actually be , be seen to happen is we'd be saying we are um uh we're combining .

So if there's causal invariants , right , then OK , if there was both multi ware invariants and causal invariants , then we have turned the universe into , I would say an O D E or something .

I mean , we've turned it into something where there's just a single thread of time and that's all there is .

It's not just a threat of time .

There's , there's one time like path .

Yeah .

Yeah .

Yeah .

But that's what I mean , there's , there's one , there's no space , there's no branchial space .

It's just , it's a , you know , we've turned it from , what would you could think of as a big sort of P D E like creature to something which is just a single variable , you know , evolving in time .

OK .

So , so it probably isn't , so multi way invariants probably isn't true .

And the argument is whether branchial , you know , causal invariants is true .

And we don't know and it , and it probably doesn't matter much .

But , but the point I'm making is that just as we can induce causal invariants , we can and do induce multi way invariants when doing things like teleportation .

Um Well , so I mean , if we could do genuine teleportation , consider an Ethiopia , right .

So , um yeah , if they are spatially separated and we want to produce a quantum measurement of the uh we want to , we want , we want to measure the combined quantum state of that , then we have to perform a spatial completion .

I agree inducing I have as much in intuition about about that as I might have about course gradient and statistical mechanics .

Um All right .

But anyway , so , so where , how on earth did we get into this discussion ?

We were talking about um how did we get into this ?

We were , oh we were talking about the significance of the valence axiom for physics .

So we're saying here that you're saying given the underlying multi way system , right ?

The claim is that a foliation which defines a total order um a vibration which goes in that case , what is the definition of a vibration when it hasn't , when it doesn't come ?

OK .

What , why is the valence aim ?

Why , why let me think .

So , I , I , I don't understand the question .

Well , there isn't a well formed question .

Um I mean , the un ai is the thing that allows you to treat these paths as being a single path .

And therefore allows so for , you know , for , for this four branched thing , this four branched algebraic structure that happens to be a finite group .

Um There exists uh there exists a foliation of this four branched structure into three branched fibers , right ?

OK .

I mean , it's not , not self evidently obvious to me but , but I mean , yes , I'm sure there is you can just , you can just have a bunch of relations that you but that combine branches .

Well , yeah , I mean that that's kind of the point , right ?

It's hang .

Wait .

Uh wait , what was the thing ?

Yeah , because like , you know , in the , in the case of a really old multi way system , right ?

So we have there exists a vibration into sort of multi branched oh Sorry , this is large and dynamic notebook .

It has enable dynamics that will help you a lot that tends to make things slower .

Uh Well , I don't know , uh maybe it doesn't OK .

What was I ?

Yes .

OK .

So there exists , you know , there exists many , there exists a vibration of this really old multi way system into multiple , I guess in this case , it's seven branched uh ordinary multi system , you know , seven .

Where did , where did the seven come from ?

Because I explicitly constructed it , I think to be seven .

Wait , OK , I saw a seven in that , but I don't know why it's some branches , something like this .

OK .

Um And so , so all I'm making is that this is the analogous claim here , right ?

So there is slow , slow down a second .

So we've got this rule graph and we're saying by what did you do to get that particular vibration ?

Well , so in this case , I'm I'm just cheating , right ?

I , I , I'm starting from the uh from the particular multi way system I want .

And then I'm highlighting that OK , fine .

The point is what would I , what would I have to do in order to construct this explicitly ?

Well , all the only point I'm making is we could just take all the branches that aren't on this fiber and make them equivalent to branches that are on this fiber , right ?

So in other words , you're saying you could collapse this real , this graph to its one fiber by either slight by either doing completions that just collapse everything onto that fiber or by doing foliation which define equivalence classes that uh make everything orthogonal to that fiber slide down onto that fiber .

Is that the same , right ?

That was , that's the whole context for this .

No , I understand that the claim is that those are , those can all be viewed as being the same now .

But they are in these finite systems , they are literally symbolically the same .

Are they not ?

Yeah .

Right .

But the , but the point is you , you have to make one additional assumption to be able to , to be able to the point is what's the difference between calling this a single branch and calling this two branches ?

But where you can kind of hop from one to the other that involves making a statement that identity and equivalence are the same thing that the fact that there is equivalence between A B and B A here on these two different branches means that we can treat the branches as identical is the statement of UN .

And does that statement have more teeth if the thing goes gets infinite somehow ?

Well , it's , yeah , I mean , it kind of , it's , it's only , yeah , it's only non obvious when you have a continuum system .

It's not , it's not about infinite .

It's about , it's about , it's about , you know , uncountability , right ?

Because in this case , they treat them as identical is kind of like , well , sure you can do that but explain what , what would go wrong .

What's the obstruction when you try and you know what makes it non obvious that you can treat them as identical when it's a continuous system .

Well , it's not , it's not obvious even in the discrete case , right ?

That's why you need an axiom of , of proposition of extensional .

What would you not ?

I mean , go ahead the notion that propositional extensional should extend to systems which are not obviously propositional like , you know , continuous topological spaces .

That's where it , that's where it gets nontrivial .

What do you mean propositional extensional ?

You mean like the aximum extensional in set theory or what ?

Uh well , the axing of it's the axing of extensional is an example of extensional .

But proposition so what is the general meaning of extensional ?

Well , extensional just means when , when do you consider two things to be the same ?

Right .

So the aim of extensional in set theory says you consider sets to be the same when they have the same elements .

Propositional extensional says that you consider propositions to be the same when one implies the other W W when they mutually imply each other , sorry that A and B are , are , you know , out of that because I , I need to remember that .

Um So , so uh I , I think I already made a note about this but I can make another one .

So it's state equivalence function in general , you know mathematics , right ?

Um So you know axing of extensional is an example of that for certain two sets equivalent if they contain the same elements , all right , oppositional extensional , all Right .

So , so , all right , what we have been talking about last time and I know you want to talk about top offers and things like that and we're going to get to those .

But what we've been talking about last time is choices of foliation that correspond to , I mean , the , the essentially the tipped foliation and the idea that you could define a tipped foliation by just adding one relation , for example .

Right .

Right .

So do , do you have an example of that now ?

So I mean that that was this , right ?

OK .

But , but how about we can see that ?

Can we see that in a group ?

Yeah , I mean this is a group .

OK .

OK .

And so then you add , so there's a group and let's just walk through for a second , both for my benefit and for people on the live stream .

Let's just could you scroll up to show what the relations are that lead to this thing ?

Well , I mean , we can , we can reconstruct it if you like .

So we take multi way group uh generators A B uh relations and start with the that they , like I said in my email that they're all converted to strings internally .

Yeah , I understand that .

I just worry about the trip in , in , into the interior , in transit now .

It should be fine .

I I famous last words , I think it's gonna , I think there are letters that you could use which would not be fine and which will just blow up completely .

But anyway , um that'll be fun to see .

OK , by the way , Nick points out on a live stream that we should update the glossary with all these meta mathematical terms .

And he's right .

Um I'll send them in to be added .

OK .

So here's what the heck is that ?

OK .

So show it in the non form first before you confuse us totally .

Um OK .

So this thing here is , let's just understand this .

This is a free group .

Yep .

OK .

So why isn't this ?

Let's understand what this picture is , which is not one of the things , this is one of the things I'm really excited about because like this is a new kind of object .

It's a , it's a kale graph but with additional proof theoretic structure which I think is really cool .

Yes , I mean , I , I hate to tell you this but I'm pretty sure these existed in a K si mean , I , I talked about this , this exact thing and I , I had a whole elaborate discussion of why these aren't kale graphs , right ?

I saw .

But as far as I could tell you , you , you did it for groups , I couldn't see any other algebraic structures .

Uh uh You mean like what like loops or something ?

I mean , so I , what I've been doing is I've been gradually just translating all , all algebraic structures I could think of into these .

I did it for groups and semi groups .

I didn't even do it for monos .

Yes .

OK .

There are monos , there are billion groups .

I , I'm , I'm working on rings and things .

Oh , cool .

Now that is interesting .

That's definitely interesting .

But , but I just want to understand this picture for a second .

OK .

So could we just look at a smaller version with labels ?

Uh Yeah .

Or the two version , even the two version with labels ?

I mean , let's let's do , why not ?

Let's do the free group on one generator .

OK .

OK .

So these are the words in the free group on one generator , right ?

Except that some of these words are equivalent .

Exactly .

So , so in the graph would be exactly .

So right .

This is the , yes , this is , yes , this is a structure that I also have long believed should exist , right ?

And whenever I've tried to feed this to mathematicians , they just tell me to go look at the graph which is this thing with all its pieces collapsed .

Exactly .

It's a graph with a state equivalence function defined by uh the right .

So this is the unrolled , you know , this is the unrolled structure of the group , the group before it has been modded down by the , by the equivalence relation , right ?

You know , before the word problem has been solved , this is the un this is the the thing without its word problem solved .

But the I mean , but you can still infer the , I mean , OK .

I , I'm preaching to the converted here , but you can , obviously you can see the solution to the word problem by .

Oh , I know you can't do any .

Yes , I'm well aware .

Right .

Right .

No , I agree .

I , I'm a big fan of this structure .

OK .

So let , let's OK .

Well , we finally get to , after all these years , we get to actually analyze this , this kind of structure .

OK ?

But , but , um uh but I think the important observation which , which really I had not understood at all was this idea of um uh of models corresponding to uh foliation of the structure .

That that's a really interesting idea .

Um But , but anyway , so you're OK .

So I agree that is that is essentially the actualization of the word problem , what you just showed .

And , and for example , by the way , in the N KS book , you will find the um uh uh a um uh a group with an underside word problem , right ?

I think maybe it's a semi group with an undecidable word problem and you can make this picture with that .

And what does it mean to have an undecidable word problem ?

It means that there are arbitrated along paths that you have to follow that , that exist in this , in this thing , right ?

Because the undecidable little of the word problem is that you can't um you know that you have to uh um it was a mistake .

That was a big mistake .

I would suggest you interrupt it .

I think I , I , I did .

Oh oh well , there you go .

OK .

That's cool .

It's a bit of a shame that it doesn't look more symmetrical .

I mean , it's fairly symmetrical , but I'm sure the real structure is , is actually uh still more symmetrical .

OK .

Fine .

Uh So OK .

So the thing I wanted to point out was so um now let's take this and we could say highlight graph , I don't know um multi graph A B B A .

So that's there and there .

OK .

So I do the abelian .

Yeah .

Right .

So if we lay this thing out or it's a partial abelian .

So if we lay this thing out in space time , branch time , so what we wanna do is we want to construct now foliation effectively where um let's construct the foliation where uh so A AAA B and B A are not treated as equivalent with respect to this partial order , right ?

Yeah .

But the where you can define a foliation in which they are and we can simulate that by taking this thing and then adding , oops , sorry , I accidentally brought up documentation .

Well , what I would suggest doing what the heck is that ?

Oh , what happened ?

Like frame apparently .

Uh And we do relations A uh A B equals B A , then we get that .

Mhm So the , so this is this is the point , right ?

So that , that foliation which would be a flat that would be an inertial foliation because it's just one uh equivalents which is then applied everywhere .

Uh defines this vibration of the system in which we treat these parts as we define more explicitly .

Let's let's go back and let's look at the full foliation which means not just one , not just two things got to be identical , but we slice everything with that sort of slicing .

OK .

So in this , in this example here , where would we put the foliation slices ?

I mean , there's many different ways places we can put them .

But what's the minimal set of places to put the foliation slices to get this initial foliation ?

Well , we just need , we , we need a , we need slices where um you know where , where , where you say aspect ratio to half for that layered golf plot .

Sure .

OK .

I think it's more revealing but only just OK .

So now , now , OK , where do you think the foliation goes here ?

Well , so you , you any anything where there , where these lie on different hypos would be a would be a valid such ao well , where , where those lie ?

OK .

So this is the claim this is morphism versus isomorphism .

There's a little bit of a story there that it doesn't that you're just saying that those lie that those are not even though in this picture those appear in the same vertical slice , right ?

You're saying they're no longer mutually independent , right ?

But what what you're saying is we need some routing of the foliation slices so that those two things appear in different slices , right ?

And your claim is that it is the only constraint other than that we can do whatever we want .

Right .

Right .

And so the point is if we properly , if , if we let that just be a general inertial frame , then so we , we know from these completion rules that if we just define rules that say , you know , A B goes to B A B A goes to A B which is effectively what these relations are doing .

It's not just going to affect that pair of states , right ?

It's obviously going to affect any pair of states that has an A B or A B A suburb .

Yeah .

So this foliation effectively gets extrapolated out to the whole rest of the multi way system .

Well , but let's see how that works .

Can we do that or how would we do that ?

How would we draw that foliation ?

Uh I let me actually get the code for this .

Cool .

Oh This is where aspect ratio has come back to bite us .

What the heck ?

There we go .

That's , that's almost right .

Well , so you're saying that , but I don't know why this is a canonical such foliation at all .

What , what , what do you mean ?

Well , I mean , why is this , what is canonical about this foliation ?

What do you mean by canonical ?

Well , I mean , you're saying it's an initial frame but you're saying , and the reason you say it's an initial frame is because there is a cosmological inertial frame which corresponds to the thing that is a certain number of , of um a certain graph distance from the root .

Right .

Sure .

But well , the actual point I'm making is that this is this is how I define it in initial frame , right .

So that , that um why do I say this ?

Right .

Yeah , free flatter inertial reference zones corresponding to what we might call free models models .

When viewers are structure , they're those defined by the axioms um or by one additional relation , right .

So , so if you just , if you , if you just have the , the um foliation defined by the axios , that's the inertial frame that , that , that's the , that's the cosmological rest frame .

Then if you have one additional relation that defines an inertial frame , is that a nice , I mean , does that work in in space time just having a single beta parameter ?

Is that , is that sufficient to define the notion of an inertial frame pretty much ?

Right ?

Are you sure , I mean , let's think about that , but you're saying that I mean , you are the one parameter families that aren't international at all and space time um not one parameter families of , you know , effectively angles of normal vectors and GEO D six normal coordinates , which is what I understand what that is .

But is that what this is as well ?

That's what I'm defining it to be .

Um We , I mean , obviously the space doesn't have a geometry defined on it .

So we , we're free to do what we like .

So in some , at some level , right ?

Um So , I mean , I can make a note of that .

So uh let's define cosmological rest frame as being um the free model to find somebody is commenting that wasn't it proved that there isn't a Cosmological rest frame by the Michael Simley experiment ?

No , sorry , that was uh that was before the cosmic microwave background was discovered .

It was the the concept that there wasn't an ether that you didn't .

The concept that you needed an ether for electromagnetic wave propagation was disproved .

The concept that there is a rest frame for the universe was absolutely not disproved .

Although at the time , nobody knew that was the case .

But in modern times , we know from the rest frame of the cosmic microwave background that there is a um uh a rest frame for the universe .

And we are traveling at about 1 1/1000 of the speed of light relative to that rest frame .

Um Does that seem reasonable that I mean , obviously , you know , in space time , you just , you just need , you just need one additional equivalence between space like separated events to define a global initial frame .

So in the same way , we define a a , you know , an inertial model as being one where there's one additional relation beyond the the sort of background partial order induced by the axios .

It's not 100% obvious to me that , that this thing about one additional equivalence relation between space like separated events is sufficient to force the frame to be inertial .

It's not obvious to me .

I think that requires some kind of proof by using , by actually thinking about um oh gosh , it might should , maybe should be obvious .

I mean , is it isn't the proof just , you know , a terror space like separated events defines an angle of a , you know , of a time like vector and geo normal coordinates .

That angle defines a global inertial frame by definition .

Well , but , but you've got to prove that it doesn't have acceleration .

What look an inertial frame doesn't have acceleration .

I know I know what an inertial frame is .

So , but that why is it self evident that the thing you've defined cannot define cannot uh must force a metric that doesn't involve acceleration .

It doesn't obviously what doesn't , it doesn't force , of course , a single pair of space accelerated events does not force a metric that's non accelerating .

But it does completely define an in a global inertial frame .

You you're saying there exists an inertial frame consistent with for , for every yeah , there is a unique global in but it's not sufficient to say that yes , that is correct , but it's not just like adding one additional group relation is not sufficient for proving that there are that there's only one additional group relation indeed .

But the thing you get out by just adding one additional group relation and just , I mean , that's what I'm complaining about with , with your straight foliation lines .

That , that's in no way , unique foliation consistent with the constraint that it should put those two values , you know , A B and B A in different slices .

But what ?

Yeah , but that , that , that's the beauty of it , right ?

So if you only add one additional relation , so you have , so if you only have one , if there's only one um equivalents made between space like separated events , then that gives you a , you know , the the , then the that that the only thing that , that you can uniquely define is a global inertial frame .

If you have space , like if you have two equivalences between two different pairs of space like separated events , then you start to get into the realm of accelerating frames and , and curvature and things like that .

No , but there are many different slicings that are consistent with the total order that you're defining here .

Right ?

Uh Yeah , that's right .

Right .

But I mean , and this is just 11 such frame as the one you're drawing .

But it is not obvious to me that that frame as you have drawn , it does not have weird accelerating features .

I I'm I'm totally confused .

OK .

So the we are the o the only type of frame that is uniquely specified by an equivalence relation between a pair of space like separated events is a global inertial frame .

Are we in agreement about that ?

The only one that is uniquely specified that has no other that yes , but I'm not , I'm but , but , but many , but the constraint that you're giving here is compatible with many non inertial frames .

Yeah .

The only frame that is fully specified by this is an inertial frame .

Yeah .

So ju just like as I say , the , the constraint that there is this additional relation is compatible with many other possible finite sets of relations that don't contain a single element .

You know , so what's the , what's , what's the problem you're making the claim that this is that you can immediately deduce from look what I'm complaining about is the drawing of these slices which I claim is non unique and not obviously consistent with it .

Being not obviously being the , the fact that you can identify those two points and say these define inertial frame .

No problem .

The fact that these slices that you've defined which in which entail lots of other relationships are .

The inertial frame associated with those things is not obvious to me .

But that , I mean , that's what I'm defining it to be .

And I'm , and like I say because of this , it's , it's exactly consistent with the definition of an initial frame in relativity .

I'm confused as to why it wouldn't be , I have to think about it some more , I'm not , I'm not , you might be right that it's sufficient to define it as that .

Um , I mean , I agree , of course , this , you know , these foliation lines are a complete fake , right ?

Because this , this network is not laid out in , in the appropriate way , but that's not the point .

The OK , I don't think we , we let , OK , but , but the main issue here is what we're saying is there exists a foliation which uh records these new relations that have been added .

And you're saying , and , and we think of that as OK , so what is the relationship between a model ?

You're saying as we add more relations , we are homing in more precisely on , I mean , a model to , to make a model , we could just say we are coordinating the space , putting these terms at these coordinate positions .

And when , you know , one term appears on top of another term that it means that there's a , you know , there's an equivalence between these things that will be a sort of a fully specified model .

You are edging towards models by adding relations , right ?

Um Well , these aren't that we're edging towards a , a complete a maximally non free model by adding relations if that's what you mean .

Yes , that's what I mean .

But even the free group is a model of the group axioms .

Fair enough .

OK .

Fair enough .

It's just like I said , it's , it's defined to be a model which satisfies no additional relations beyond the axioms of a group .

Fine .

OK .

Fine .

So , but what I'm saying is that in normally in , you know , you can , you know , when you go far enough .

So , so actually something , I don't know , it's probably obvious , you know , you take a group , I call the heal group , whatever you want .

A five , whatever it is , right ?

And it has a certain set of generator and relations .

Let's say you incomplete , add the relations .

What do you get a different group ?

What's that ?

A different group closer to the free group ?

I see .

I see .

I see .

But it might not be a finite group .

That's the point .

That's , that's why we don't so much know about it .

The point is you need a certain set of relations to guarantee finite and probably by the time you've hit finite ness uh even even then you might go further .

OK .

So fine .

So what will happen is you start with a free group , you keep adding relations .

The thing will at some moment it will become a finite group .

Um Right .

And , and the sorry , go ahead .

No , no , I , I was just gonna say , and obviously we , we have the , we have the model of the free group and we also have the model of the maximally non free group .

Well , in fact , I actually have a picture .

Yeah .

Uh somewhere it takes a moment to render because it's quite a complicated object .

But basically , you know , you take some algebraic structure , you apply all possible kind of completion rules to it .

And therefore you get the maximally non free version of that algebraic structure because it's now that structure , it's the free version of that structure in which all possible relations have been applied .

And how does that relate to the royal graph ?

Well , that , yeah , that , that's the point , right .

So the the graph is the maximally non free objects .

That's why we consider it to be the fundamental structure .

So this is an example of a group to which every possible relation has been applied .

So it's the maximally non free group .

Right .

But now that object if we looked at the graph of that object would just crush down to one point .

Am I ?

Right ?

Right .

Right .

Everything is equivalent to identity .

So , so all the the life and times of this thing is in the non manifest equivalent of different words .

Right .

Right .

So the the , you know , obviously the the fundamental point I mean it's kind of obvious but we should probably note it anyway , you know , the free group is maximally quantum mechanical or purely quantum mechanical .

The maximally non free group I E in which all possible relations slash completion rules .

Pride is purely classical or no , no , no .

About all uh I can't say regular ordinary groups um lie somewhere on the quantum classical spectrum .

Yes .

Um So this Ral structure is basically the Ral structure of an arbitrary binary operator with arbitrary binary operator with inverses and so on .

What else does it have ?

That rule structure has the underlying group axioms ?

But here's but , but I mean , here's the interesting thing , right ?

So that so in this again , preaching to convert it , I know , but the nice thing about these objects is ultimately , they don't make a distinction between the group axioms and the relations just like because multi systems don't make a distinction .

In fact , they don't make a distinction with the generators , either the generators are just unidirectional relations .

And so the point is um it doesn't , once you get to this structure just like it doesn't , you know , once you've generated the rule or multi way system for some model of computation , it kind of doesn't matter what the underlying model of computation was .

By the time you've generated this thing , it doesn't matter what the underlying axios were .

The point is every algebraic structure that can be defined as I understand has a limit point , which is this , it's a limit point under repeated completion is that yes , exactly .

And so by extension , every algebraic structure that's based on sets with binary operations satisfying some axioms is a fiber in some appropriate vibration of this space .

I agree .

But , but the fact that it's binary operators is important this thing , the geometry of this thing will be different but it's not binary operators .

No .

Exactly .

So , so which is why I'm actually quite excited to produce the ring version of these , um you know , once we start looking at rings and modules and algebras and things , it will get more , you know what we got .

Yes , I agree .

Um So , OK , so I , I have to say , I'm just stunned by how beautiful uh like the free abelian groups are .

Um uh So it generates is , no .

Yeah .

How much does it matter that the thing is a subgroup rather than a semi group , by the way ?

Uh a little bit .

Well , we can , we can see that explicitly .

Hang on .

Make a 3d picture .

Let me do three steps .

I get more interesting .

Yeah , it's interesting .

But now I just do graph 3D of that .

Okey dokey .

I don't know , just make another picture .

Don't , don't destroy that one .

Just 3% .

And what ?

And then we're gonna look at the summit group , right ?

Yeah .

And oh my gosh , what the hell is that ?

What is that ?

I don't know .

Hang on .

Let me do .

I think this might get , I forget which one it was that had some very nice symmetrical structure .

I mean , that's gonna be huge .

That's gonna be huge .

Stop , stop , stop , stop .

Absolutely huge .

We shall see .

So .

Hm OK .

Give it a moment .

There we go .

Well , that's nice .

It's lovely .

Yeah , I , I really like this .

Yeah , there's some nice wall arts to be made here .

OK .

So , so anyway , but this is the rule , this is the completion limit .

Well , sorry , this isn't , this is just the obedient limit .

But so , um so to answer your question , if we , if we take a multi semi group , those two generators , uh A b uh-huh quotes , right ?

Relations , none to so the , so the semi group is kind of boring if we don't have any relations , right ?

Because it's just each element kind of acts completely independently .

Um But if we start to add , I mean , do you want to take the obedient kiss ?

So if we do something like that , then it starts to have more interesting structure , right ?

But by , by semi group , you are doing , you are going both ways because the the the natural multi way system is a semi semi group .

What what the natural multi way system ?

What is a semi semi group ?

It's one where the relations don't go both ways around .

Well .

Oh Yeah .

Yeah .

OK .

Sure , sure .

No , they , they , they do go both ways around in this .

OK .

Fine .

So your thing is defined to go both ways around , right ?

Because it's a semi group .

OK .

So can we just see the corresponding picture there for multi way multi way group ?

Just the exact same thing ?

Just make a copy of that , just make a copy of .

So , but we also need to do the E and versus and multi group , multi group and so good catch it gives you some indication Ok .

Hm .

Well , of course , uh alienation .

Did , did you want to see the aliens version ?

Because defining A B equals B A doesn't Abel this , right ?

Because we also have to because there is , there's A B and there's , there's more , more , yes .

Right .

So we really want the A version .

OK .

Well , the Abel version is just the free Abelian group , right ?

That's just let's do states graph structure .

That was the thing we were looking at earlier .

Oh Jose on our live stream says he's actually written a paper about the free wing group .

Oh Cool Cool .

Uh And as an intermediate , we could say multi a mono .

Uh Well , actually let's let's do the free case first .

So this is all going to give me a further complex about the N K S book that everything that was in there that was partially explored actually needed to be taken further .

Um OK .

So that's the , that's the free case of the mono .

But then if we do , well , actually , I , I should have a , I should create functions for doing a billion versions because I don't have that right now .

Uh OK .

That's equals E A uh B E equals E B and you have E squared equals E already .

Uh e Well , we could do that as well .

Oh Sorry .

Ah No , this is the problem with using symbols .

Yeah , that , that is a problem with using symbols but you know , it should have E squared equals anyway .

Yeah .

OK .

All right .

So let , let's zoom out back , back again to what we're talking about .

So we're talking about the fact that um OK , so we've got this notion of models and we've got the idea that um by we can make these foliation that , that add equivalences effectively .

And your claim is that un valence , the un axiom is the statement that uh we can as well mathematically .

I mean , I , I still claim that the fundamental point of the valence axiom is mathematics only cares about answers .

It doesn't care about working that .

That's the fundamental statement .

It , in other words , you can , once you've established an equivalence , you can throw away all the working inside .

Do you agree with that statement ?

That's , I mean , that's an an implication of it .

Yeah , I agree .

But , but the question is what's the essence of it ?

So in physics , it's like saying you can see when you say it's an equivalent , what what you're saying is you can deduce things about the world by even if you've coarse grained , you can do things about the world .

Yeah , it's just cose graining , right ?

I mean , that's the essence of it .

It's that once you know the macro state , you can throw away the micro structure , right ?

But , but , but , but the fact that you can throw it away , the reason that that is a meaningful statement , I mean , the reason that's a contentful statement is , is because you care about the theorem more than you care about the proof .

What I'm saying is that you can , you can then build your mathematics doing only that similarly , you can build your physics looking only at the coarse grained states , right ?

I agree , right .

But so it is not self evident and it is a consequence of , you know , causal invariants or the or the uh you know it that for OK , two statements , either there's causal invariants or there are observers who induce causal invariants .

And either way it's sufficient to look at the , the causally moded states to know how to build the physics that you care about .

And similarly , in the mathematics , what we're saying is it's sufficient to , I mean , operationally what it means is in doing mathematics , you care about theorems , but you do not care about proofs to , to , to build your mathematics .

You can , you know , once you've proved something , it's like it's like the Tetris game , it's already disappeared and you can go on and build further in the tower .

Is that a fair characterization ?

I mean , that's , I'm just trying to get an intuitive understanding of what this means that , you know , like I say , I , I , I think as we talked about last time , I , I agree that's , that's an implication , right ?

But the , the , the question is that is a , what is it about mathematics ?

Because the fact that mathematics is doable , right ?

If it wasn't for that , you know , in , in studying cellular autometer , I want to contrast the mathematics of studying cellular autometer with mathematics as it is normally done .

And you know , I think the , because mathematics builds up lemmas and C A s don't .

Right .

That's , that's what you're saying .

That's what I'm saying .

What I'm saying is that in C A S you care about the innards of what happens .

It is not sufficient to just say , you know , this is the the input output pair , so to speak .

I mean , I think we all agree on that , right ?

I think that mathematicians define lemurs .

Yes , I understand .

I , I it may be obvious , but I think it's a fundamental piece of philosophy of mathematics which had not been understood , at least by me before now .

Um the um right define lemmas and cell automaton operatives do not so to speak .

Um OK .

But , but then what we have been coming to last time was OK , we had been , we were close to having a good understanding of the analog of special relativity in these things .

And so let's just recap that .

So the analog of special relativity is the statement that uh there are well , OK , different frames correspond to different relations being added , right ?

So OK , well , so OK , so we're , we're saying that given a , I mean , that , that's a , that's a OK , let's , let's um I mean , that's the statement , let's walk through that claim , but we , we can also walk through the claim that different frames correspond to different foliation that correspond to different editions of relations .

And we're saying that the basic claim is you , you're claiming that this quantity is invariant with respect to that , that is you can either verify the theorem by walking down the explicit proof graph as defined this .

What are we calling this ?

The , it's , I mean , it's basically the multi way graph .

But what is the mathematical statement of that ?

The , the explicit abstract proof graph basically ?

Or you can say , let me define a model , verify the model .

I'm not sure what the analog of verifying the model is .

And , and I mean , you know , in space time , we don't think there's anything to verify in the case of an inertial frame , we're just like it's OK .

But you know , we can set up an inertial frame , I guess that's in Minkowski space .

So it's not obvious .

Well , in G R , it takes irreducible computational effort .

Yeah , to , to , to , to confirm that you have a valid choice affiliation to determine that the points in your acclaimed space like hypo or in fact with the partial order indeed it does , right ?

But the question , OK .

So I I just want to , OK .

In general relativity , I understand that you're that what you're doing there is to trade off the establishment of a valid sequence of specialized hyper surfaces with the , which is the model val validation are against the actual sort of following of the , these , these edges .

Um But let's see , but there are more things that are true .

OK .

But what is the analog of Special Relativity ?

What is the analog of the Makowsky or isn't there one or is it only , what's the analog of special authority ?

Well , the , the , I mean , the , the statement has reduced to initial model to , to initial models models with only one I know , I know .

But is that , but is there a clean version of that ?

In other words , can we , can we quantitative derive , what is the analog of the quantitative , you know , one minus V squared over C squared ?

What's the analog of the E equals MC squared ?

Um Well , with E equals MC squared , I I I don't really understand what you meant by the derivation of it in the spacetime case , given that it's a definition but um but it's not a , it's a definition of rest mass .

But the question , but there is an intuitive sense of rest mass .

Sure .

Right .

That's the , that's the question is whether there is a definition here that , you know , sort of aligns with the intuitive notion of arrest mass .

Right .

So , so I mean , the question is look and in general , but I don't even know in , in the OK .

Again , special activity .

Is there a , is there a clean notion of special activity as opposed to general relativity ?

Yeah .

OK .

So , and your claim is that , that is the one relation case .

Yeah .

OK .

Well , let's see that , I mean , so if that's really right , then it better be true that that one relation .

So what's the analog of velocity ?

Um What do you mean the analog of velocity is the , is the distance in the proof , you know , is given by the distance in the proof space of the two sides of that relation , obviously .

Well , it's saying that the two sides of that relation , let's imagine that we put them in , we put them in two successive elementary time slots .

Is that going to be our velocity that we take this spatial distance in proof ?

Uh No , it's not right .

It's not quite right .

It's not quite right .

OK .

Look proof space .

OK .

First question is what's distance in proof space ?

OK .

Distance in proof space .

How do we measure distance in proof space answer ?

We have , you know , we have this multi way graph .

OK ?

Defining points presumably that's let's let's OK .

So this isn't quite the same thing .

So OK , go ahead , go ahead , go ahead .

No , no , I just I I'm recapping what we discussed last time .

Uh the number of necessary .

Well , OK .

So this is this is distance from the route is a coordination which is essentially like in the like the time in the cosmological rest frame , right ?

Bye .

This is .

So you should write that down , you should make a note this is time difference than the cosmological rest frame that the difference between two terms the the time just is an invariant proof time interval , which is there just to be clear that this is the distance that you have to go down in the multi way graph to get from one term to another , right ?

But now what does that have to do with ?

OK , fine .

So that what , what is , what is it ?

This isn't a distance , this is a coordination .

Well , it's also a distance , it's a coordination .

If you start it from the Big Bang at the beginning , how does it , how does it give additional coordinates ?

It's giving one coordinate , right ?

The number of applications uh You , you're saying that , that you , that you take a , if there was only one axiom , it would just be AAA linear order of how many times you have to apply that axiom .

Yeah .

OK .

So if you have multiple it , OK .

So let's walk through that .

So that if it's a binary tree , for example , the leaves are labeled by binary numbers , right ?

That's the analogous thing , correct ?

OK .

Yeah , you , you agree , I mean sure that that's so we have 22 theorems that two axioms zero on one and the each leaf is labeled by the , by the sequence of , of uh of , of axioms you needed to do to get to that leaf .

Yeah , I understand .

Yeah .

OK .

So OK .

So let's again , I'm trying to understand what is the derivation .

How can we derive ?

Is there a quantitative version of rents transformation in this case ?

Well , yeah .

OK .

What is it ?

It's the lens transformation .

It's the thing that preserves the , you know this invariant interval .

OK .

Can we write down what , what the formula for it is ?

So in terms of that proof time distance , right , we have the the , you know , we have the speed of light which is the , you know the maximum proof speed .

Yeah .

Right .

So what is , what is our formula for , you know , can we can we write down what I mean ?

We should be able to transform , you know ?

OK .

So in the holds in spaces of any dimension , yes , I I understand .

But so can we figure out what it actually means in this case ?

Right .

So you , you've made a claim that the relation we can describe what the velocity corresponds to relation is by looking at the distance spanned by that relation effectively .

OK .

So what you're claiming is if we look at the distance spanned by that relation and we compare it , how do we compare that to the quote speed of light play ?

I don't understand .

There should be OK .

So listen , if we're trying to get for example time dilation which you're claiming you would get by taking successively in in your model in your setup , right ?

As we take modding out relations that take that span larger distances .

What we will be getting is essentially higher velocity frames , right ?

OK .

So it should be the case that as we get to a higher velocity frame that , that the , that when we do that , that the essentially proof time necessary goes up by this Pythagorean .

OK .

Yeah .

OK .

So that would be an interesting thing to see because it is a quantitative relation that we get by saying we are picking a particular relation that's then implies something about the number of steps that we have to go through for a particular proof , right ?

It's saying I , I agree , which is why in the very first live stream , I mentioned it would be interesting to find out what the model theoretic analogs of slowdown theorems would be , right ?

But so currently working on OK .

OK .

So , so , so this is , so this is OK .

So , so this is not a totally stupid question .

It's just you haven't figured out the answer yet .

So , no , I , I , I agree .

It's not a totally stupid question .

That's why we asked it several days ago .

I'm , I'm wondering what the with you because I'm slow and I work on other things in between these live streams .

Um The let's , let's go back to this again for a second because I think we're actually , we actually could kind of crack it , right ?

So , so what we're saying is there is a certain distance , I'm just saying , what is the comparison ?

There's a certain distance in this metric , right ?

In your , OK , you've got a multi way graph it , you label every , you can label every node in the multi way graph by a possibly redundant sequence of , I mean , it's essentially the word length in the , well , it depends how you set it up but , but it's , it's a , in the multi way graph , every element can be labeled by , it's essentially part number in how you got to it .

Right .

Yeah .

Right .

Which is in general redundant .

There may be multiple paths to it but there is a shortest such path , right .

So you , you could label it if you want to label it with different axioms or you could ignore the different axioms and you could just say it's such and such a number of steps from the root , right makes sense , right .

So , so what we're saying is a a given , you know two elements which are joined by a , by a completion by a relation , right ?

They will each have certain coordinate positions in that coordination , right .

Yeah .

Right .

OK .

So now , now we've got , so we've got two , you know elements which you are going to conflate with a , with a completion , right , with a relation and they are , they are at two different coordinate positions , right ?

They're about to be conflated .

They will define in your claim of frame right ?

That that corresponds to that has an effective certain effective velocity if those proof relations were OK .

So here's a , here's a point if those proof relations were time , like if those terms were time like connected , right , then that would be the equivalent of a speed of light transformation .

No , it would be a superluminal transformation .

If they were light light connected , it would be a fine , what does it mean ?

OK .

So what would it mean for them to be light , light connected ?

Well , I mean , that's what I , that's what we discussed last time , right ?

And that's what I was writing up here .

Um So , you know , here , if you consider an elementary proof cone , you can consider the extrem or points just like you would in an ordinary causal network .

So then the light like parts of the nonconstructive proofs , the ones which require infinite computational efforts in order to witness the associated model and the internal ones , the time like paths trying to trying to understand , OK , I still , I just think there is going to be some formula that basically just tells one in terms of the distance between things which are being connected in a relation .

There will be some quantitative formula that tells one the effect of slowdown in proof uh-huh , right .

And that formula would essentially tell one as one looks at a theory , right ?

As one , as one turns a knob to change one's theory , right ?

That that's gonna tell one as you add axioms that effectively connect more and more distant points or more and more uh well , closer and closer to the time like connected points .

What does that mean intuitively as you connect those things ?

I would expect that it would make proofs go faster but it doesn't , it makes proofs go slower according to this .

What's going on there ?

In other words , OK .

I would have expected that if you make a lemma that lets you jump ahead , for example , in my boolean algebra thing , right ?

Which , which it obviously does , right ?

Because you're , you're increasing the theorem , you're decreasing the theorem verification complexity by increasing the model verification complexity .

That's why I wrote this down .

OK .

But , but , but so intuitively , what one's saying is by adding a lemma which is a jump ahead lemma .

You are effectively .

Why does that ?

What's confusing me is time dilation is normally something where things happen more slowly , right ?

It takes more steps .

Oh No , I see the problem .

The problem is the definition of the time coordinate you , you appear to be going more slowly but time passes more quickly for you .

Right .

Right .

That's , that's what I'm confused about .

Right .

So the , so the answer is we're decreasing the theorem verification complexity as I said .

Right .

Right .

Right .

So , so what you're doing is you're trading off you trading off theorem verification complexity for model verification complexity because by adding in the lemma , you're reducing the length of the shortest proofs , but you're adding in an extra step and verifying that that additional lemma is in fact .

So , so intuitively , what you're doing is you're by , by adding a sort of jump ahead in the in the theorem network , right ?

You are making it faster for you to get further in the theorem network .

But to somebody looking from the outside that means time is passing faster for you but you uh right .

But every but , but so what does that mean for ?

What is it , what is the outside observer ?

What is the observer at rest in the mathematical and meta mathematical world ?

What is the observer at rest as compared to ?

So the observer at rest is saying is the free model ?

No , I understand that .

But the the observer at rest says that uh oh you're time is passing , why do , why does the observer at rest ?

Say time is passing slower for ?

Oh I see , I see , I see because , because they are able to get further in a given time , that means time is passing slower for them .

Yeah .

OK .

OK .

That's right .

That's just exactly the same .

And um but then the claim is there is a quantitative connection between time .

Yeah .

All right .

OK .

I mean , I , I , I , I still think there's a , there's some actual , you know , V squared over C squared thing .

But do you agree or do you think that that's not correct that there's an actual , you can actually measure this as in you can actually measure of course , but of course , he can , right .

But so so you should be able to see it .

For example , in , in other words , what this should do is gosh , we might even have the data for this in , in the N K S book .

Needless to say I did this thing of adding Lemos , right ?

Adding I did here .

OK .

OK .

You you can shorten proofs by adding , you know , you you can , you can achieve a speed up of three steps by adding only a single lemma at the expense of in increase of increasing the computational complexity of verifying that the lemma you added was compatible with the original set of vaccines .

But in particular , this means that that as you add lemmas , so this is kind of like the speed up of mathematics , so to speak , as you add lemmas , the question is , you know , as one publishes more theorems , what does this mean ?

You know , how should mathematics speed up as more theorems are published ?

And what ?

Well , I , so a as the uh you know , as the technical sophistication of mathematics increases A K more theorems are known , right ?

A K more theorems known a generalized graduate student who is prepared to take these theorems .

Yeah .

On faith can perceive more quickly .

But the task of uh you know , formalizing all of mathematics gets more complicated that true .

Yeah .

OK .

OK .

So then , and , and in particular mhm uh fair enough .

So what else should we ?

I mean ?

OK .

OK .

So OK .

So what's the , what's the story of , of , I mean , if we look at mathematics as it now exists , what is it like in terms of , I mean , like , you know how close is it to Minkowski space ?

What , what um you know , what is the curvature ?

You know , what , what is if we look at mathematics as it exists , which I've tried to do , you know the three million published theorems roughly that are known .

What , what can we say about the , the structure of that space ?

So in other words , we could have started with a most minimal mathematics , we could have started as um yeah , what , what is it , what you know , we could have started with universal algebra or something and then we are adding , how , how do we think about , yeah , how , how do we think about mathematics as it has been ?

So as as soon as somebody comes up and says , I , I want to think about groups , they had an axiom about that which molds down essentially universal algebra , right ?

Sure .

So the question is what is the analog between , you know , the human choice of adding these random axioms that correspond to group theory and things like that ?

What has that done to the shape of meta mathematical space ?

Well , it's covered it , right ?

You say it like it's totally obvious .

Yes .

Each , each additional relation is defining a new possible angle for the , for , you know , for , for this um time like vector and ge normal coordinates .

So the more of those you add the more arbitrary curvature you get .

OK .

So let's , let's Jonathan , you , you just see the , you make everything sound so totally obvious .

I agree that this is the direction .

But I think to , to the statement that new Axing systems of mathematics correspond to curvature of mat mathematical space is not a self evident statement .

I mean , it may be now self evident , but uh fair enough .

A adds each relation adds a new um unit normal direction to a proof like hyper surface .

So what you're saying is that , that , that what this is sculpting the proof like hyper surfaces .

And , and your claim is that with just a single relation if mathematics was universal algebra , well , what that isn't even the base , what is the base , the base of the base , the base of the base is just the language without any , any anything with no relations .

No , it's the set of all symbols , right ?

So that's the base of the base which , which itself is not well defined , but we won't even worry about that .

Right .

OK .

So , so what you're saying then is that every , every time we add , you're saying you're sculpting the proof like hyper surface by adding an additional capability for it to be deformed in a new direction , right .

Right .

So it's the , it's the point OK .

E each relation is defining an equivalence .

Each new relation is defining an equivalence between a pair of proof like separated points , right ?

Yep .

Um I uh and wait a minute , should we be calling them proof like separated ?

Because they're really the space like separated points .

They're , they're branchial , separated points .

Yeah , I'm so I'm calling the proof like separated because they're proof theoretically independent .

That's the , I mean , that's the key thing , right ?

Um I agree .

It's not a perfect analogy .

Well , let's see if there's a better word .

Um I mean , what would be that deduction is the word that corresponds to time deduction corresponds to time .

What is orthogonal to deduction ?

I mean it's really independent .

Yeah , it's , yeah , they are , they are independent .

OK .

Fine .

Let's , let's just say um proof theoretically independent terms um which defines a hyperplane who's normal .

Um But yeah , OK .

It which defines a hyperplane considering it's normal , gives a unit normal direction to some hyper surface .

I'm not sure this is the best way to think about this .

I mean , so , so that each new relation , let's see , it's defining what is the analog of adding new relations in and OK , in , in ordinary physics , the analog of of is the point , right .

So in , in ordinary relativity , um I want to try to sculpt a space like hyper surface .

Yeah , by , by doing clock synchronization between distinct points .

Right .

Right .

So , so , so , so yeah , exactly .

So I , I have to try but I , I only have a discrete set of clocks and I have to try to interpolate a hyper surface that's consistent with that .

Exactly .

Can you write this down ?

Because that's a good point .

That's a good , I mean , that , that's , that's what's going on here .

This is pair wise clocking , you know , pairwise equal .

What , what we're doing by adding each relation is a bunch of power wise uh synchronized clocks uh spacetime foliation while only having access to a discrete set of clocks in particular pairwise spec .

Yeah , with respect to which to do uh pairwise synchronization .

Is it a whole , is it a whole clock or is it a single event , aren't you doing pairwise synchronization of just events ?

Uh Yes .

Yes , you are instant discrete set of uh I guess in , yeah , discrete set of events , right ?

So what we're doing is crucially there are events with , you know , with a time tag .

What do you mean a Cosmological rest frame ?

Time tag ?

Yeah .

Right .

I mean , so , so , well , no , e each , each event , it's what , what you have is not a clock but rather an instantaneous clock , right ?

It's , it's a , it's a , a space time event but which , which hasn't , it has a well defined time associated with it .

Where did it get that time ?

Well , the same way a clock , same place a clock gets that time , which is from where in this , in this view of the Cosmological rest frame or what , or just the clock evolving from ?

Don't get time from the Cosmological rest frame .

They just get , you know , they , they are intrinsic generators of time tags .

But only once you've started the clock .

So if the clock pre existed from the time of the Big Bang , it will have ticked a certain number of times before it reaches you .

Right .

Right .

But AAA clock , what is the analog here ?

This is a clock .

What , why do you say that this has a a um why , why does it need an intrinsic time tag ?

All it's saying is that these two um uh pro the independent events are now considered to be time like , right , you , you're now you're defining those two events to be , to be in time like relation to each other .

You're saying that those two events which you wouldn't have otherwise known that they had any wait , what , what I , I , I , I , I completely don't understand .

So I , I , I give you in ordinary relativity , I give you a discrete set of events that are not time tagged .

How do you do synchronization ?

What does that even mean ?

I'm saying what you do is you say you got these random events in space time , right ?

And I'm saying this event is , you know , I'm going to define this event to be a time like successor of this other event on what basis ?

And why is that synchronization ?

Well , I think that's what you're ending up doing here .

And I think that it's not easy to do that synchronization , which is the point you're making .

I mean , in other words , that that's really not easy if you don't have any , if you don't have clock information , you can't do synchronization .

Or at least I I'm not aware of any possible procedure by which you could , you , you can't synchronize , you can't do a sort of permanent many slice foliation synchronization , you could only do one slice .

And I think this isn't correct here .

I think that the analogy then that's not synchronization .

Then , then you're just taking a collection of events and saying they lie on a hypos .

That wasn't what I that's not right .

But I think the reason is that in this case , as soon as you add a relation , you're not just adding a relation in one place you it's extrapolated over the whole space , right ?

Which is , which is right , which is , which is why .

OK .

So in fact that this time tag isn't the relevant thing .

This thing is more like a clock because what's happening is that it's saying um all paths of events , it's a little confusing , it's a little confusing because it's , it's basically it's defining , I don't know what's confusing at all .

You , you you you have a selection , you have a discrete set of events with a time tag which you can think of as being an instantaneous slice through the time like extension of a collection of clocks , right ?

And then all you're doing is you're saying we can define a synchronization and then let's extrapolate that synchronization .

You know , the , the , the hyperspace foliation you get from that synchronization over the entire proof time .

I don't quite get this .

So try try this again .

OK .

So , so um uh OK , you know , imagine a collection of clocks uh extended in time .

So , so these are , these are time like curves that you know , have , have the time like curves traced out by clocks .

Is that correct ?

Right .

Right .

OK .

A bunch of time like curves traced out by cocks fine .

And on that time like curve , the clock is is chopping is making ticks on the time like curve right and take a discrete set of slices through these , you know time like extenders the PS right .

So then what you get is a bunch of instantaneous clocks .

In other words , what you obtain is an instantaneous I is is a , is a discrete set of events with time tags , right ?

Fine .

OK .

So , but this is this is kind of what I was , you know , look these time like curves allows us to do a discrete version to , to to con to , well , yeah , to do a discrete approximation to standard relativistic , right .

OK .

So let's just let's just clarify what we're talking about .

OK .

So we have time like curves that potentially start at the Big Bang and on them live clocks on these time like curves , they're marked off in certain unit in certain intervals , right , that correspond to the tick of the clock .

We are then saying that the space like hyper surfaces are those surfaces which , which join identical uh tick numbers on those time like uh curves , right ?

OK .

So now the analogy here is , let's carefully go through the analogy here that every , OK .

The analogy is that every completion , every , every , yeah , every , every association of tick number 317 on one time like curve to tick number 317 on another time like curve is like the association of one end of the completion to the other end of the completion .

Yep .

Right .

So each one of those , so then as we add a completion , OK .

So the , the , the those two time like curves have tried , they , they define one , I mean , I think you , you may have said this already there's one vector in space time that joins each one of those things .

And that is defining a , that is the one piece of the spacelike hypos service that is so far known from those two clocks is that single vector , right ?

And so you're saying , as we add more vectors , there are more embedded vectors that must live inside the space like hyper surfaces .

And in general given a single vector , we could perfectly well have flat space like hyper surfaces .

Other than that , you know that , that , that their direction is defined by that vector .

But as soon as we throw down other random vectors , we can no longer have flat space like hyper surfaces , right ?

You get curvature , although it's a slightly weird way to get curvature because what it's saying is that there is no longer a flat hyper surface consistent with those relations , right ?

It those relations force you to have a curved hyper surface .

Yeah .

Why , why , why is that a weird way to get cover to ?

It's just like saying , you know , if you have some random collection of points in the plane , then it won't generally define a line .

They won't generally , I know , I know , I know it's just a little .

OK .

But fine .

So we've got these , we've got these , these um these edges , if you wrote a note about this , it would be helpful .

But I mean , you know , we got these , these sort of finite vectors in that join these things and they , um OK .

And in fact , we could even do that .

I mean , in one of our , in , you know , all we have to do is um uh you know , we actually can draw these things which you in fact had in one of those previous pictures you actually had drawn with the , with the graph layout , you had drawn something which effectively corresponded to those .

Yeah .

OK .

Um Well , that we knew but yes , um they OK .

But OK , so then as we add more mathematical facts , we are sculpting these uh proof of independence , these independence surfaces , right ?

So what , so if we were to add , so what does it mean ?

For example , if we were to add some uh um you know , hike , what , what does it mean when we , for example , if , if we're so , has there been a black hole added in mathematics ?

In other words , we're , we're adding curvature by adding um axios , right ?

Are there any axios that have been added ?

Which , which force the black hole or the Axion of choice ?

I thought you were gonna say that .

Let me understand why .

So because you're saying because they force proofs to be nonconstructive in its vicinity .

Let me understand that .

So you're saying , I mean that's a very interesting statement if , if OK , so the question is right , the axing of choice uh permits nonconstructive proofs .

And therefore you claim it is a thing with a which has light like I'm , I'm a little bit confused by that , that so the axiom of choice defines vectors that are light like vectors .

Is that the idea ?

Well , OK .

So , so the the acting of choice is , you know , so , so interpreted as a basis vector on proof space .

Uh So crucially , it permits nonconstructive proofs .

But there are , there are examples uh and in particular uh permits proofs of propositions that would be undecidable by any constructive means , right ?

There are things you theorems , you can only prove using the Axion of choice in a nonconstructive way in which it would be independent if you .

So the claim would be that that vector defining the axing of choice is a light like vector when it permits the existence of um paths .

Well , interpreter is a effect on proof space .

The aim of choice uh permits it's not , it's not that it's , it's not that it is a like , well , I mean , it's not that it itself is a light like vector , it's that it is , it produces a collection of paths where attempting to follow any of those paths necessarily forces you to be , you know , to , to follow a light like path .

The A O C defines a family of necessarily light like paths .

OK .

What , why let's think about the gery of that ?

What's the analogy in relativity ?

Well , an inventor , why does that force light like paths ?

That's what an event hori is , right ?

It's the , it's the place where all paths necessarily become light like , well , the , the , let me think about that for a second .

So your claim is the event horizon at a conventional central horizon , light cones tip over such that uh to remain at the boundary would require that you be on a light light curve .

I agree with that , right ?

But I mean , otherwise you just cross the event horizon .

I mean , if it's a black hole like event horizon , I mean , any kind of event horizon you have to be at , you know , you have the light light curve is the thing that skims the event horizon , right , right .

So the point is that the the event horizon is a family of paths that are consistent with the causal partial order but cannot be followed by any subliminal .

So look likewise claim the axing of choice defines a family of paths like like oop sorry that are consistent with the causal partial order E G defined by Z F C or E G two , sorry E G defined by Z F .

Right .

Exactly .

Uh But cannot be followed by any subliminal model by any constructive model corresponding to a computationally bounded observer or corresponding to a computationally bounded mathematician .

OK .

Let's walk through this for a second .

OK .

So by the way , we should add some Luminal to our spelling dictionary .

Um The uh uh um submit , what's that ?

Yeah , subliminal is the only one to look at .

Um Unfortunately , it's a close word and it's always , it's always annoying in spelling dictionaries to think about the redundancy of these things .

OK .

Anyway , but , but back to the different topic .

OK .

Um OK , let's think about this for a second .

Defines a family of light light pas So what does it mean when you add this ?

So what we're saying is any one of these axioms is adding a , you know , it's here's the question , right .

So , so , so suppose you wanted to prove a proposition or prove the proposition that two terms , you know , that , that one term on an event horizon implies another term on native horizon on the same that horizon , right ?

Such a proof is necessarily nonconstructive .

Well , by which we mean that there is no completion that , that , that the only way to do that proof is to follow the underlying uh um I mean , let's just walk through what we mean by that .

The only way to do the proof is to follow the follow the underlying multi way graph , like the underlying proof graph .

I , the theorem can be proved syntactically , right by following the explicit light .

But there is no model in the system but no model lying in the interior of OK .

Hold on one second because the intuition behind constructivism is the model .

You know , you've got enough model that you've kind of saturated it to the point where the model really is about something , right ?

Our models though are a little bit more sliding scale , right ?

In other words , normally in constructivism , you , you , you , you want to have , in other words , you know , you're saying , well , the free group is a model .

Well , it's , you see what I'm saying ?

Yeah .

Yeah .

Yeah .

So , so constructivist care more about these , wait uh you know about these kinds of structures where you're like where , where there are examples , you know , the kind of maximally non free structures , right ?

That those are the things that these are sort of the idea that that's what this , you know , like this um uh Kesler orders and , and like , you know , I tried to study this in the book , how close does an axiom system come to defining that ?

There's only one model that's consistent with it .

In other words , to what extent is it about something ?

I don't know what that is .

Oh This , this is about this regards um regarding uh Axio systems that define unique models only up to , you know , define unique models up to isomorphism .

So I looked for such a theorem 2025 years ago or something .

I didn't find it .

Is that an English English theorem or is that like old as the hills ?

It , it's quite old .

So it's a bit like it's very much like the lo Scholle theorem in its , in its construction , right ?

So , so , so what , what , what Molly is essentially saying is if you have uh if you have a theory that I may get the statement slightly wrong , maybe Matthew can correct me if , if I get it slightly incorrect .

But basically what it says is um if you have a , if you have some theory and it defines um it defines a model of some infinite cardinality .

Uh then the by morally categoric , uh there is only one unique model of any , you know , any infinite cardinality up to isomorphism .

Sorry , say that again .

Say it again .

What ?

So , so it's like I say , you know , a bit like how the loss the is , is telling you effectively that , that , that finite theories can't control the cardinality of their infinite models , right ?

Remind me , remind me uh it's without me looking it up in the book , what Los Column theorem is .

Sure .

So if you have a theory that's , that's made of a finite collection of sentences and it has a cardinality of the sorry , it has a model of some infinite cardinal , you know , some , some infinite cardinality , then it will have a model for all infinite of size , for any infinite cardinality .

OK .

In other words , that , that , that , that if you have a finite collection of sentences that isn't sufficient to kind of nail down uh the cardinality of the , of its right .

It splits out just like in the girl's theorem .

It splits out and has an infinite finite yeah collection of sentences with a model of size , some infinite cardinality .

Yeah , it will have a hierarchy of , of , of size four or size K for any infinite cardinal .

Is that right ?

For any infinite cardinal or just an infinite collection of infinite cardinals .

I believe it's any infinite cardinal for , for the full Scotland case again , I'm , I'm , I'm relying on our resident logician to jump in and correct me if , if , if I get something , if I say something stupid .

But um so more categoric again , my , my recollection of it is uh if you , yes .

So again , if you have a finite collection of sentences , you know .

So if you have some , some theory and it defines um well , essentially what it does , I , I forget , I forget the precise technical uh sort of hypotheses you need .

But , but essentially it gives conditions where uh you can have a theory that defines a uh AAA sort of some infinite model .

And you can prove that , that , that this infinite model is unique .

I see up to isomorphism in , in certain cases , OK , there exist taxing systems where you can do this in some cases , right .

So , so this is why , so this was used in this came up in that paper on on orders that you you forwarded to me , right .

So , so this is why kind of why are the real numbers so annoying to work with ?

And the complex number is so beautiful .

Well , it's essentially because the real , you know the the the real numbers as a dense linear order , your claim have lots of possible models whereas the complex numbers have a have a smaller number of models , right .

Right .

That it is is far from being unique , whereas the complex numbers are unique up to isomorphism as a closed algebraic field I see of characteristic zero , right .

Right .

Right .

Uh as guaranteed by lyrics .

But I would like to understand this better because that this is a this is an interesting result and , and it it , I think it does have good , you know , interesting things to say about what we're doing OK .

So hold on .

But , but this is , this is asking , OK , we , we're still back to the event horizon and the aim of choice , right ?

I have to say that the number of , I , I bet if we search on the web for aximum of choice and event horizon , I bet the number of hits of those two concepts being in the same place is very small .

But if it isn't , then somebody's discovered something interesting .

Um The real question , if it isn't , what's the probability that Dana Scott is the reason why ?

There's no , he doesn't do event horizon .

He , he doesn't do event horizon .

No , no , he's not physics oriented otherwise .

Otherwise , if , if one , if one gets to anything where there's , um uh let's see who the logic meets physics crowd .

Um oh my gosh , there might be something here , systolic aspects of black hole entropy .

Somebody writes about um systolic .

Well , that , that's a term and , and um I've only ever heard that in , in the context of like the vascular system .

No , no , no , no , no .

It's , it's also used in the , in the context of V L SI design of um uh it's , it's essentially a causal graph related story .

I haven't a clue why it would , where it would show up in .

Um uh um OK .

Well , I will , um I found I found one example from um oops , no , no , no , no , no , no .

The word choice is appearing with the word axiom , but it is not axiom of choice .

OK .

Never mind .

Um Oh , well , OK .

All right .

Um OK .

Question .

Um OK .

So let's , let's go through this again .

So , so the claim is that the axiom of choice forces that OK .

By the way , there's a question on our live stream from Alison asking about distinguishing positive and negative curvature .

Hm Yes .

Right .

So G E six , do you increase or decrease proof redundancy basically ?

Right .

Posi positive , you write that down positive curvature is increasing .

Well , yeah , increases proof redundancy bow out lots of different proofs or curvature but I guess increases proof diversity increases the diversity , theorem diversity but proof proof redundant but not .

Um so , so in other words , a theory with positive curvature is , is one that doesn't where , where there are a few , it's like the the elephant or something knows a small number of , of uh of big facts .

The fundamental theorem of algebra is probably a high positive curvature region of meta mathematical space .

Well , but let's let's understand what this means .

So positive curvature means that you are concentrating , you're , you're focusing a lot onto a small number of you , you're focusing on to certain certain theorems basically .

But um or alternatively , you're saying that the number of inequalities that exist because we're really talking about equities here .

The number of qualities that exist is comparatively small as opposed to negative curvature where you make a make a note of that .

The , the , the um oh yeah .

No , no .

Yeah .

Right .

There's a different statement that the number of equalities um that increases their diversity .

What increases theorem diversity ?

You know , I I E number of equalities .

Yes , it is larger number of , in equivalent number of distinct equalities in equivalent equality sounds too strange .

Yeah , it's larger number of number of distinct .

Um But so that , that is saying that um so let's talk about that in terms of what that means .

So , OK , so if we add a theorem , if we add an axiom um or lema whatever it is that , you know , one of the things I had in the N KS book was a list of things people say about theorems .

Like that's an interesting theorem .

That's a powerful theorem .

That's a surprising theorem .

What do those mean in this theory ?

So for example , a surprising theorem I had imagined connects to regions of meta mathematical space that are otherwise disconnected , right ?

Uh A surprising theorem conjecture .

Well , here a short path connecting apparently distant points in mathematical space right here .

Let me just um find my uh let's see .

Um Hold on , let me just find this .

Uh um oh Come on , why didn't I put that in the index ?

Surprising theorem should have been in the index ?

Um um I've got all the stuff about uh let's see .

Oh Hold on .

I , I just want to find because I've got a nice list of these , these different cases .

Let's see whether our search system is not totally terrible .

Ah , here we go .

Ok .

Here I'll put it in the zoom chat and pull it up .

Ok .

Uh , hold on .

Well , if I can figure out how to do that .

What are you doing ?

No , no , no , I didn't want , I didn't want to open the zoom .

I only have one monitor .

I didn't want to open the zoo .

It's um it , it does , she doesn't , it , doesn't , it , the way it works is it's um OK .

It is not recursive .

It's , it's some , OK .

Here we go .

So here are some , a difficult theorem .

A theorem having a long , having only a long proof , I guess that's interesting , elegant theorem short and somewhat unique .

I don't know if that's right .

So , I mean , I had a lot of notions about how things , how connected things would be a deep theorem , right ?

AAA G D six segment that appears at the start of many other G D six segments possibly .

And that's Euclid's axioms .

I mean , Euclid's elements .

What on earth do we learn from that ?

I mean , remembering that that's only , that's only a single connection between theorems there .

That's not the network of all possible proofs .

Who knows ?

OK .

In that case .

Um All right , let's go back to your screen .

I , this , this is um I was gonna see if I could out obscure you with a , an even weirder .

What Uh Wait , let me see .

Do I have this ?

Oh Yes .

Oh Sorry .

Oh Go ahead .

This is the associate .

This is the equivalent plot uh for intermediate theorems in Spinoza's ethics .

What ?

Well ?

But that , that's from a single proof , right ?

No , no , no .

This is for all .

So I systematized all part all the arguments in , in um in Spinoza's ethics and proved all of them and looked at the lemma distribution and proof length distribution in those and did some analysis on it .

Oh Did you post this blog post or did ?

No , I keep meaning to but I keep getting distracted by other things .

But yes , I , I , I will at some point soon how Minoza only had that number of things in his , in his .

Um th this is only book three .

I did it as an illustrative example , but I , I , I did this particular one because it's the one that has the , the , you know , the , the , the money shot the , which is the proof of the necessity , the necessary existence of God , which takes 214 steps at least in the way that I formalized it .

Yeah , we'll just wait until we can do this .

You know , we're gonna get closer as we understand meta mathematics more .

We're gonna get closer to the proof that the proof of the independence of the existence of the universe .

That's gonna be exciting , right ?

I I'm , I bet that can be done .

I agree .

But I think , I think we even have a scheme for doing it but we should , which we keep meaning to discuss .

But the , ok .

Well , anyway , I mean , I don't know what it means if we can prove the independence of , of the existence of the universe .

Um , yeah .

Well , anyway , um , ok , the was , I mean , hang on since we're , since we're on it just as a , just as a sort of rough scheme .

So this , this is how I claim I , I , I think it could .

Why are you , why are you putting it there ?

And I don't know , I think you should put it at the end and existence of the universe .

We're gonna be totally confused .

The ax independence of Yeah .

OK .

Um So if you say something like um OK .

So , so you , you give me an argument of the form uh X implies that the universe exists , right ?

That , that would be a , that would be a , an explanation .

Yep .

So how do I go about verifying whether or not that's true .

So , first of all , what I need to do is so it's exactly the , the reason I wanna , I think it's useful to discuss .

Actually this now is because it's exactly this model verification question right there .

So there is a universe out there and there is the universe referenced in your argument .

But how can I confirm , which is a model of the actual universe ?

How can I confirm that they are isomorphic , right ?

OK .

Hold on , hold on your , your argument tells me that a thing that you have called the universe exists , I think you should say universe with capital U , OK .

There is a universe but that isn't with a capital U that implies that the universe exists , there is a universe out there .

How do I determine the universe ?

Right , which is the model of the actual physical universe ?

Right .

Right .

OK .

Yes .

So , so basically , yeah .

So , so , so um in other words , validating your argument is a problem of model verification , confirming that universe equals equals to the universe .

OK .

So now consider the analogies of the second and completeness theorem .

So consider second and completeness theorem which says that um so the consistency of piano arithmetic is independent of piano arithmetic .

And the way you prove that is you say um well , to prove consistency of P A would require enumerating all uh you know , all , all , all semantically true propositions in P A or require enumerating sorry , all tactically provable proposition positions in P A and demonstrating that there are no contradictions .

Yeah .

But by first incompleteness theorem , we can't do that right .

No such enumeration exists .

OK .

So I claim that there is an analogous thing here that prevents you from that , that essentially prevents you from doing this model of validation .

And so the , so the the , you know , so analog of first incompleteness theorem for physics uh you know , you can't know the outcome of , of the , of the evolution of the universe .

Right .

Right .

So , so you um we can construct a good , a physical , good sentence by building a physical computer whose program says if you know , if , if the rule for the universe halt or something .

Uh Yeah , predicts that this program will do X , then do Y otherwise do X Y .

OK .

So intuitively , it's just saying that we can't , you know , figure out the infinite time outcome for the universe , right .

Right .

Um Computational universality prevents us from uh you know , from computing something about the universe in a strange pun of words from , yeah , from computing features of the universe , infinite time features of the universe faster than the universe itself evolved , right ?

And rough .

OK .

So OK , fine .

So we've got that .

So then , so my claim is just like valid , just like proving consistency of P A requires enumerating all syntactically provable propositions , proving that universe equals equals universe requires uh enumerating all physical systems entailed by universe .

And demonstrating that this set is in 1 to 1 correspondence with the set of physical systems in the universe .

But physical incompleteness .

OK .

Let's walk through this enumeration can be made .

OK .

So the claim is that scroll back up for a second .

Um So let's see .

I don't know why you need this X implies that the universe exists .

I think what you need here is uh let's walk through what you mean by universe with a lower case U , universe with a capital U , the universe with a capital U is our particular universe .

Right .

Yes .

Right .

So I mean , my , my , my point is what , what would an argument for the existence of the universe look like ?

Well , ultimately , it would start from some hypotheses and it would say therefore the universe exists indeed .

So , so any such argument can I claim can be represented in the form of X implies that the , OK .

So what we're saying is , is there an axiomatic basis for the statement that the universe exists ?

That's really the making that because that's what that , that's what this means .

Is there , is there an axiomatic way , is there a way from to prove from mathematics that the universe exists ?

Is there a proof based on formal axiomatic transformations that the universe must exist ?

Right ?

And the answer to this is about to be no , there isn't , there can't be such proof would have this would necessarily have this form , right ?

OK .

So we've got axioms that purport to prove that the universe exists .

So now maybe it's uh uh yeah .

OK .

Fine .

Imagine those axioms and ask the question .

Um So OK .

So may , may , maybe it's easier , maybe it's less confusing if I don't call it the universe , right ?

So , so you know , we , we say something like the , these axioms .

OK .

So , so ignore this , these axioms imply that this structure called X necessarily exists is I don't call it X because you just said X implies the no , no , this is why I'm bracketing this off .

So you structure called a structure called U necessarily exists is U isomorphic to the universe , to the physical universe , right ?

OK .

And for that , you claim you have to enumerate all possible things in the physical universe to verify that , right .

So , so what does it mean ?

So what , OK , it's back to extensional thing , right ?

So , so the the axiom of extensional for universes , right says that you have to verify every element in the universe , verify that the universes are identical , right ?

Two universes are isomorphic if and only if uh every physical system inside them is identical , right ?

OK .

So now assuming that the universe is infinite , assuming that the universe has an infinite time history , you can't ever do this .

Sure .

But I had a normal form .

I bet you could do this but not from within the universe .

No , but that's , that's then a statement of computational complexity , not a statement of uh you know , in the infinite time case , you just can't do it .

Well , you , you don't know this is the thing why this is the nice thing about this good sentence because you don't even need the infinite time limit .

This just says as long as you're inside the universe , you cannot construct this , you know , you cannot construct such a computer otherwise it will contradict .

I think what this , what this , what this says is if you think there is an axiomatic proof that the universe exists , that is , it's never going to work .

In other words that the from within the universe , you can't , you can never , the statement that the universe exists will always be independent of whatever Axio Axio system you set up that purports to show that the universe exists .

No , you , you can't give a proof from within the universe that and an axiomatic system establishes that the universe exists , right ?

So let's just understand what that means .

So that means that , I mean , it's , it's hardly surprising that you can't mathematically prove that the universe exists .

That is hardly a surprising fact .

Um But it means that in any system of axiomatic deduction , you know , this question of , of um uh you know , if , if I ask , why do electrons exist in our theory ?

What's that ?

In what sense ?

Which , which aspect of what kind of ?

So he had , he had this um famous rebuttal to Anselm's ontological argument that existence is not a valid predicate .

Oh yeah .

And so this , this is proving the physical version existence is undecidable predicate , right ?

Existence for physical existence is an undecidable predicate is a mathematically undecidable predicate .

Even though we think we've reduced physics to mathematics , we still can't .

I mean , ba basically what is mildly surprising about this is that , you know , in our effort to make these models we think we've reduced physics to mathematics basically .

But yet the question of , of why that physics is instantiated , we can't answer from mathematics , we can answer about the physics , but we can't answer why it's instantiated .

Right ?

OK .

Good .

Well , that was , that's a good little piece of metaphysics there .

That's a nice result .

Yeah .

OK .

But , but OK .

Um OK .

But so , so we , we were talking before about axiom of choice and its and its role in event horizons .

And the question of whether and the , you know what the actual landscape of mathematics today looks like , you know , does it look like a galaxy with a big black hole in the middle ?

What does it look like ?

What is the , you know , what , what areas of positive and negative culture are there ?

What is the , so in other words , what what we're saying is we humans just like we humans place things in the physical world , we think with free will .

But who's to say um you know , that arrange the physical world to have some particular form ?

So similarly , we're placing things in the meta mathematical world that make the meta mathematical world have some form and those things that we place have consequences for meta mathematics that we may or may not immediately understand just like , you know , when we place things in the physical world they entail there are laws of physics that , you know , if , if we decide to , I don't know uh you know , if we decide to pull the moon closer to the earth , there will be , you know , put rocket engines on the moon to move it closer to the earth , there will be physical consequences to that , that we could potentially calculate , so to speak .

Um So similarly here , as we add something in meta mathematical space , it , so for example , you're saying , I mean , so what would get us totally tangled up in mathematics , in other words , is it inevitable ?

So if , if we think about the future of mathematics and we think about , you know , the addition of essentially landmarks in meta mathematical space , what do those landmarks ?

I mean , what , what can we say about the , about the nature of those landmarks , for example , you know , am I making any sense ?

I mean , in , in um yeah , but sorry , I , I've gotten distracted by the first part of your question , you know , um and I'm now wondering whether there's a relationship between .

So , you know , how in , in sort of , in , in , in philosophy of mathematics there , there's this hierarchy of , of conceptions like , you know , constructivism uh finite is ultra finite is and things like that , right ?

So uh so they , they , they kind of go progressively from , from weak to strong .

Um And I'm wondering whether you sort of et cetera uh is there a correspondence to the hierarchy of causality conditions ?

And she , because so effectively , you know , constructivism is saying that you can't have uh you know , you can't have black holes .

So that's making , so that's putting a causality condition about , you know , future extend ability of time like J D six effectively finite is then putting additional constraints on curvature .

Ultra finite is putting even stronger constraints on what does say .

So finite says that you , that AAA any infinite , it rejects the existence of any infinite mathematical object .

Um ultra finite is rejects the existence of mathematical objects that are finite but too big .

OK .

But so what does OK .

So these are , for example , like actually , you know , finite is , is kind of part at least partly motivated by physics , right ?

It's saying that there is a maximal theoretically computable natural number given the current age and energy density of the universe .

And so , you know , any steps that have cardinality larger than that cannot have existence .

OK .

So , so let's look at what that means here .

So what you're saying that means here ?

Yeah .

Uh And that rejects , you know , yeah , un feasibly large but finite mathematical structures , un feasibly large but physically large in a sense can't be , you know , un feasibly slash un physicals large .

OK .

OK .

But so , so again , let's walk through this .

So , so we're saying that um you're saying , what are you claiming about that ?

It would , I mean infinite mathematical structures .

So that why is that not saying that you can't have an infinite time like curve of some kind , I don't know what that means .

I mean , what is an infinite mathematical structure in this , in this context ?

So it's , you know , as we were discussing before in these algebraic cases , right ?

You start with a , you know , if you start with a free group , it's , that's naturally an infinite object .

If you apply enough relations , it becomes a finite object , right ?

If you apply more relations , it becomes a smaller finite object and so on .

So these are placing conditions on how many cons it's placing limits on how you know how many constraints you need in order to have a valid model .

So it's saying you can't just have an , an abi you know , some , some model of arbitrary curvature .

There are actually by , by the way , yeah , I mean , when you have a finite group , that means there's positive curvature .

Yeah .

Right .

Right .

Because I mean , this is completely obvious but I , I wasn't , I wasn't internalizing that , that a finite to achieve a finite group , you know , to achieve a finite convergence , right ?

Require the convergence of distinct G D six in the associated free group .

And he , right .

So , so basically the point is that when you have positive enough curvature , right , then what you're doing is you're , you're , you're , you're finite the the meta mathematical universe , you're making the meta mathematical universe .

I mean , just like we believe our physical universe might , you know , probably will expand forever and so on .

We could perfectly well have a purely finite physical universe , which is what we're saying would happen in these cases where , you know , you , you could have it so that there's essentially enough mass in the meta mathematical universe to cause it to be finite .

That would have to be the claim there's enough mass .

I mean , you could write that down because I mean , basically what we're saying here is that mass , which we , which we said multiple times here , mass slash energy is the equivalent of more mathematical knowledge .

So this is saying when there's enough mathematical knowledge , you are forced to have um essentially a finite , you know , if you think , you know enough about relations in mathematics , you will end up with a finite structure , right ?

And , and the fact that mathematics is has infinities in it is a consequence of freedom in mathematics , so to speak , right .

So your curvature conditions is too weak , right ?

So in other words , in a sense , you know , be careful what you wish for because you know , if you , if you prove too much in mathematics , the your universe will collapse , right ?

That's basically what one's saying here is that if we're not proved too much , if you assert too much in mathematics , your universe will collapse , right .

Right .

We should make a note of that so that we don't forget that that claim , I mean , you know , in other words , that that term you add too many actions .

Well , I guess relations collapse branches is the point you're making .

Yes , but otherwise no one has .

But also they , they make for the whole space is finite .

I mean , the whole of mahe mathematical space then becomes finite .

There comes a point at which sufficient collapsing , right ?

So , so in particular , we know in group theory , right , that , that is the point at which a group becomes a finite group .

When you add enough relations , you can make it a finite group .

Yeah .

I don't know whether , if you just sort of add group relations at random , I don't know what happens .

Do you know ?

Uh , yeah , I mean , I , I , so some of these relations I was adding , um , oh , I , I didn't , I don't think I have the notebook open .

I sent you some pictures of things which , which were , uh , monos and things where I basically added relations at random .

And , uh , and yeah , eventually they , they become , I just wonder whether anything else can happen whether , whether the end result , if you just add relations is that they always eventually become finite or that they may become essentially inconsistent .

They may , they may get to the point where there's only one could , you , could , they become inconsistent ?

No , they , they , the , the , the worst case is there are so many relations that they've gone that they've crushed down to essentially 11 distinct word .

Right .

Right .

That all words are equivalent .

OK .

But go , go back to the end there .

Sorry , going back to your thing at the end .

Um So sorry , it's , it's some .

OK .

So the claim is as you add more axios , you increase the mass density of the meta mathematical universe which causes you to have more positive curvature , which would one might think before you reach finite .

What you're saying here is you say before you reach finite , OK .

What , what you would think from the relativity analogy is that as you add mass to the universe , before the whole universe essentially collapses , you will at least locally have a bunch of black holes .

Sure .

OK .

And a and a black hole in mathematical space would correspond to somewhere where there is an event horizon which I mean , you know , like the classification that we've tried to do of branchial of enters OK .

What , what does it look like when you have a , a brachial of enter horizon ?

Um You're saying that you can't cross , you can't make a foliation that crosses that hence you can't make a model .

Yeah .

OK .

That , that I think makes sense .

OK .

So , yeah , so non constructivism , we claim it's still not that the axioms do , do the axioms inevitably produce an event horizon .

Does the , when you throw the axiom of choice into your meta mathematical system , does that inevitably produce uh an event horizon ?

As I mean , as long as you , as long as the acting system you throw it into is sufficiently rich .

Yes , I think so .

Why , because mean , why ?

Because it will produce proofs that could only be con , that can only be written in a nonconstructive way .

Well , I understand that , but that's just the statement .

Well , ok .

Ok .

Ok .

Ok .

Well , ok .

Well , we managed to cover lots of stuff .

We spent a long time here .

But , but , um , uh , and , um , um , and was there a direction , I'm , I'm sorry that just , just to , it's kind of like three hours later , what was our actual agenda ?

Um What was there a direction that you were trying to go ?

That was , I mean , I I thought this was very useful , at least as far as I was concerned that we're understanding this better and better .

Um Sorry , I was , I was because I was trying to think of an easy example .

So the the best example I can think of is um sort of an obviously non constructive theorem .

Yeah , like , you know , a certain digit occurs infinitely often in the decimal expansion of pie or something .

OK .

Well , it's there isn't a nonconstructive theorem .

It will be a nonconstructive proof .

That would be a , what do you mean a nonconstructive theorem .

So , I mean by that , I mean a theorem where there is no constructive proof .

So , I mean , there are plenty of examples of theorems which have both constructive and nonconstructive proofs .

But what you need for an event horizon is a theorem which has only a nonconstructive proof , right ?

Where the only path is a time like is , is a light like path which would be the , you know , the the path .

So let's walk through what that means intuitively , this , this theorem .

No , the sorry .

Yeah , maybe I should say a theorem with only a non , with only nonconstructive proofs .

Probably we don't know whether that , I mean that that could have a constructive proof that that statement could have a cons what , how , what ?

Well , the fact that there are , you could , you could say the proof that there are an infinite number of primes could only have a nonconstructive proof and it isn't true .

There's a perfectly constructive proof of that .

I , I , I can't say offhand that there's no constructive proof of that statement .

Hm I think it's likely , I mean , in other words , for twin primes , it could be that there's no constructive proof .

Could it be that there's no constructive proof ?

What is the measure ?

OK .

Fine .

Fine .

Let's , let's go , let's go overpowered .

OK .

OK .

Fine .

That's how I'm pretty sure it is nonconstructive .

But what does it mean ?

I mean , is it the case that I wonder if Matthew is still with us ?

If , if Matthew was able to unmute himself , he could actually opine on the subject .

Um I , I am with you but um I don't think I'm any help in this case , Matthew , you are , you are , you are playing the perfect logician here um but is there , is there a way of thinking about um in terms of standard mathematical logic , how does one think about non constructive proofs in kind of the , the um traditional treatment of mathematical logic ?

Is there a , well , usually people refer to the pro the , the reason why I'm not helpful here is because I , I uh I , I , I don't use intuition logic .

I , I don't use intuition logic .

I don't use constructive logic .

You died in the Wool Lord of excluded middle axiom of choice .

Kind of fussing and , and , and , and this is because my , my undergraduate degree , my bachelor's degree was in physics .

So , so I have sort of sort of a physicist's point of view of logic , by the way .

Sorry .

Can I , can I just comment how , how wonderfully paradoxical it is that someone who has essentially dedicated their career to understanding computable of the laws of physics and things is a , is a nonconstructive logician .

Yes , I don't know why .

I just find that .

Very funny .

Yes .

The um what's the relationship between computable and non constructivism ?

Is there one ?

Um Well , th th this is realizable and uh you should talk probably to Andre Bauer .

OK .

Can you summarize what , what is realizable ?

Um You should talk to him not to me .

OK .

The OK .

Can you make a note that real liability is relevant to this ?

Do you know what it is ?

Jonathan ?

Uh So I , I've read a bit about , I mean , I , I've read a bit about the , the broer hating of interpretation that , you know , this intuition stick interpretation or the , the real interpretation where you know , you , you , you have a constructive mathematical proof and this additional constraint of real allows you to extract more information from it by essentially assuming that the proof is computable .

Um But I , yeah , that's , that's about the extent of my knowledge .

I see , I can see why that would be relevant to Hoopy type theory and so on .

And that , that whole program real slash B H K interpretation .

Talk to the bow .

Yeah .

Right .

Um OK .

OK .

But , but yeah , I mean , so at least to this kind of hand wavy intuitive level that , that I , I'd say they're definitely related , right ?

That , you know , constructive mathematics is all about proofs that where you can construct a uh you know , a computable model that witnesses that proof .

Yes .

Right .

And there's more subtlety , subtlety to it than that , but that's what is a non computable model .

Well , I mean , you know , a model involving sort of uncountable cardinals and things would be , right , would be non computable .

But , but I mean , so OK , so again , with respect to what we're saying here , hour , the , the basic claim is that again , axiom of choice introduces , I'm still a little bit confused about what , you know , in other words , we're building mata mathematical space , we're putting things down in matta mathematical space .

And we're putting down these , these equivalence vectors basically in mata mathematical space .

And what do we , what do we do when we put down the equivalence vector for the axiom of choice ?

What does it , what's special about it ?

Why does it , why does it force ?

So , so it's , you know , so , so obviously we , we , we have , you know , generalized Einstein equations higher the I , I'm , I'm gonna keep , I'm gonna continue using this word abstraction .

I mean , hoping that you know what it means in the sense that , you know , I don't think it's quite the right word .

But yeah , the , the , the , the higher the level of mathematical knowledge , the , the higher the level , the higher the level of mathematical knowledge fine uh the more the more proof redundancy that's , you know , that's what the Einstein equations say .

Right .

Yes .

And intuitively that's because the more proof redundancy because there are more proofs that wind up going to the same point , right ?

The higher the level of mathematical knowledge , there's more mathematical knowledge that takes you , there's more different ways to do the same thing .

So then the claim would be the axing of choice is too powerful .

It produces so much mathematical knowledge and induces so much proof convergence slash redundancy uh that , you know , that , that nonconstructive becomes inevitable .

OK .

Let's walk through that for a second .

OK .

So the claim is that the axiom of choice has too high a itself represents too powerful , a piece of mathematical knowledge .

In other words , it's too high , a piece of , of mathematical mass .

Yes .

As too much mathematical mass .

Um So , so , I mean , here's , here's one way , I guess you could think about it , right .

So , so there's um there's a growth rate of mathematical knowledge that's inexorable as you go down the proof graph , right ?

And there's a growth rate of constructive proofs .

The axiom of choice is powerful enough that it boosts the growth rate of mathematical knowledge , the growth rate of knowledge to be too fast , too , so much that the growth rate of non sorry .

Yeah , I say the growth rate of constructive proofs cannot catch up , right ?

So what does that mean ?

So that means by constructive proofs , we mean proofs that have , that are constructed by using models that are more or less saturated models in the sense that they're actually about something ?

Is that right ?

Sure , actually .

Does Matthew have an opinion about that ?

Is that a fair characterization ?

I mean , when you talk about constructivism that there must be degrees of constructivism because this whole question about whether it's a model about a definite thing .

Go ahead .

Well , no , I I'm just gonna say uh again , I'm not the person to ask about constructivism .

OK .

Fine .

Um No , but is , isn't that right ?

Jonathan ?

That , that there isn't , it's not like you're constructive or you're not cons isn't there a question of Well , no by constructivist explain in our context what it really means to be constructivism to construct constructive for proof .

It means that the proof is being done by looking up , looking down the sequence of foliation rather than by looking at the partial order .

Yep .

OK .

But the problem is the sequence of foliation is you know , you can have , you can have more or less total , so to speak in your , in your foliation .

That is , yeah , I mean , and there is , there is a hierarchy of constructivism as you say is there , I don't know that .

Yeah .

Yeah .

Yeah .

I mean , like , so , so for instance , um you know , intuition is , I mean , this is just an example that I happen to know a bit well is so in , in intuition is um uh permits the principle of explosion .

What the heck is that uh that , that's , you know , if you , if you have one contradiction you have infinitely many .

Oh I see , I think because it's , it's fancy time fancy term .

That's , that's the stupid claim that that false implies anything .

It's not totally stupid .

That's kind of stupid .

It's , I mean , that's , that's kind of what's , that's the definition of a contradiction in , in classical nonconstructive logic fair enough .

OK .

Um So where , whereas other , no , sorry , whereas other constructivist mathematics is do not permit it .

That's , I mean , that's one example .

So intuition is a , is a brand of constructivist mathematics , right ?

But so So you're saying there is a how constructive you are , you can be more or less constructive , which is what I would expect from this .

Right .

Right .

And , and , and we actually , you know , this gives us , so , so we , we , we can now with this formalism , you know , we can , we can put a measure on , on how constructive something hierarchy of constructivism , both in terms of uh computable and computational complexity theory of the associated models .

Yeah .

Right .

So OK , so then that means OK , so intuitively , what's happening with the axiom of choice is it is it is making it really difficult two um have foliation .

Yeah .

Yeah .

I mean , it , it's , well , it's adding , you see it , it's not jumping ahead infinitely , it's jumping ahead finitely .

Um Well , it is kind of jumping at , I mean , the , the the point is that if you were to follow the time like path on the event horizon model theoretically , that would take you infinite time , right ?

It's just that the partial order allows you to , to reverse it in finite time .

So it is kind of allowing you to jump ahead infinitely but only infinitely .

But , but with respect to our models .

So how would that show up in our models where we are creating these models by doing completions ?

That , that would be saying that if we've added those completions , let let's just walk through that for a second .

If we added some of those completions , why would that prevent us ?

Can , can you see , you see my question ?

So the creation of those models is a story of adding those completions , right ?

Yeah .

OK .

So why does adding those completions now prevent us ?

So now we've got a completed well proof .

Go , yeah , go ahead .

No , because the point is if you have the axiom of choice , then there is no finite completion , you know completion sequence .

So with A O C for each critical pair , you force to converge you get more , I know finite completion .

And why are you , why are you saying that ?

Why is that true specifically about the aim of choice because of its non constructive , right ?

Because if , if , if there were a finite completion sequence , then you could construct OK .

So , so , so what you're saying is what you're saying is that I E model construction is not , is is undecidable , it is non computable .

OK .

So you're saying there exist certain kinds of axioms which if you were to add them and they probably are related to axiom schema in , in the world of you know , ay is that right ?

That there that there exist axioms which if you add them , you can't get a finite set of completions to cover them .

But is that related to Axio schemas ?

Not in any direct way that I can see .

What , how would you , well , what , what is the characterization ?

I mean if I pick a random axiom , OK , you know the induction axiom of piano arithmetic .

Let's say if I pick a random axiom , how can I tell whether it is going to induce , uh you know , a , a nest of , of , of critical pairs or not ?

Well , that's the problem of determining whether the word problem is decidable , which is difficult .

Well , yeah , go ahead .

What you're basically asking for is analogous to saying here's a presentation of a group .

Tell me whether or not the word problem is decidable .

No , I realize that .

But I'm asking , I'm asking we should be able to classify axioms .

Certain axioms do not have this property , they do not induce non constructivism .

And they also in your interpretation , you're saying that the induction of non constructivism is associated with the , the in the production of an infinite collection of branch pairs , I think so .

OK .

Did you make a note of that ?

Because that's , that's a , that's an interesting claim , right ?

That's why I said , right .

OK .

Well , but with A O C in particular , but the claim would be that for any axiom , I mean , we , we , we're using A O C as the sort of shorthand for any nonconstructive Axion .

OK .

Fair enough .

But you're saying for a nonconstructive Axion for an axiom that induces nonconstructive is that it is a generator , it is a non causal invariant .

It is a , it is a thing that produces branch pairs that is , that forces non causal invariants that will be a claim .

Yeah .

And as I say , my , my reason for saying that is that if this weren't true , then you could induce a , a cos in variant model , which I think would violate the claim that it .

OK .

So , so the very interesting claim is that if you introduce rules that are not causal invariant , right , if you introduce Axion , that are not causal invariant , that they will force nonconstructive proofs , well , it's not , it's not that they're non causal invariant .

It's , it's a step higher than that , right ?

It's that they can't be made causal and variant .

Well , OK , they're not , could you write a note of that ?

But that , that , but they're non comple A O C is an example is a potential example of a , of a non comple maximally non causal variant , right ?

And I E non , not finitely comple so , right , I said , OK , what the heck is no finite completion procedure ?

What , what causes there to be no finite completion procedure ?

Well , if there's too much branch , but I know that .

But what , what characteristic I mean , can we write down ?

OK .

Can we write down just with A's and B's and C's ?

Can we write down something , you know a string substitution system which has uh which has no finite completion procedure ?

I know you were just saying you were just saying earlier , right ?

That you have examples of groups where there's undecidable word problems ?

Yes .

But what's the relationship between that ?

And OK , the , the the question is this , how does Knuth Bendix , what , what this is saying is the Knu Bendix procedure will never terminate among other things , right ?

There isn't a completion procedure , right ?

And your claim is that whenever there's a , there is a , if there is a finite completion procedure , then the word problem is decidable .

Yeah , Ken terminates so word problem decidable .

So all I , all I'm saying is the converse is the contra positives of that , right ?

So in what sense is , so what is the relationship between non decidable of the word problem ?

And , and , and aim of choice or other so called non constructive axioms ?

Where where do you see the , the undecidable of the word problem show up in connection with that axiom ?

I don't know , I don't know .

I mean this is saying that the proof network , the non undecidable of the word problem could be thought of as a feature of that proof .

What , what does it mean for the proof network to say that the word problem is undecidable ?

I think it means it means there's no upper bound on the length of , you know , even for a bounded size of , of word , there's no upper bound on the length of the path that will reach that , that , that word ?

Right ?

Well , let's think about that .

So , so why ?

Yes , but um this is a slightly different thing that there's no upper bound in order to even reach you know a word of length four or something .

There may be no upper bound on how , how far you would have to go to reach a , reach a um uh who I went for ?

What is this ?

What is this claim ?

What is this the thing you just wrote down ?

I'm just this , I mean , I know I could read what you said .

What , what do you mean ?

So the , the , the condition of the causal graph , you know , limits to a finite dimensional manifold , a manifold with , with fixed dimension in the limit is some condition on how , how much it can bifurcate , right ?

If it bifurcates at every step , it it's gonna grow to some exponential dimensional thing .

So , so the point is the ability to apply a completion procedure is some is some con constraint on the multi on the proof network branch .

And so given that this is the thing that allows you to say that the Einstein equations are satisfied in the continual limit .

It may be the case that the satisfaction of the generalized Einstein equations uh for the proof network implies that you necessarily have constructivism that , that , you know , you can't have so much branch that the uh that the , you know , isn't guaranteed to terminate .

Well , it's an interesting claim .

I'm not sure I'm convinced by that .

But if that's the , this is conjectural , the , I mean , I would think , well , OK .

But the , the , the main point here is what this is doing , look , look another way to say it is the following .

The undecidable of the word problem is a consequence of the fact that there are unbounded long paths necessary to verify even comparatively simple words .

OK .

Which is to say in terms of our jumping ahead idea , that's to say that there is arbitrarily long reach ahead , so to speak , there's an infinite hierarchy of reacher heads that this axiom can do .

See what I'm saying .

Mhm I think that's the point .

I think that's the , that's the issue .

The issue is is there only a , you know , when you write down , when you try to write down the completions that correspond to a particular axiom , is there only a finite , you know distance of reach ahead that the thing can do or is it an infinite reacher ahead ?

Right .

So in other words , what that means is the axiom of choice is allowing you essentially to prove .

Um Yeah , is , is , is allowing you , I mean , all we're saying is the same thing we're saying .

It allows you to make infinite jumps forward in , you know , it's allowing you to make infinite jumps in the original proof golf .

Uh You know , it's allowing you to make an an infinite hierarchy of infinite jumps of , well , it's allowing you to make an infinite hierarchy of jumps forward in the original proof graph , which is to say that it is , and that's , well , you're saying that with respect to the original proof graph , there is no model with the respect to the original proof graph that can reproduce that behavior .

Mhm Although there is a model , if you assume the axiom of choice , you can get a model , right , right .

It's just from , from with , from without having the axiom of choice .

But so what is the statement about non constructivism with the axiom of choice ?

Normally you're saying that if you there are theorems that you can prove only non constructively without the axiom of choice that you can prove constructively with the axiom of choice .

Is that right ?

That would be the claim .

Although , you know , usually it's , it's not the the the the set of actual nonconstructive theorems in this sense is , is quite small , right ?

Usually it's just the axing of choice gives you nonconstructive proofs of theorems that could be proved in constructive ways .

No .

What , what it gives you nonconstructive proofs of theorems that could otherwise have been proved in constructive ways .

You mean not having the axiom of choice gives you that no having the atom of choice gives you the possibility of producing nonconstructive proofs that could otherwise have been proved .

Oh I see .

I see , I see , I see , I see , I see .

Fair enough .

Well , OK , do we have a , I mean , just , you know , before we wrap up , do we have a road map of where we're , what we're trying to ?

So I think what we , what we've established here is we've got , we can essentially measure for , for our automated theorem prover as mathematicians , so to speak , we can measure their .

So we're emulating , we're recapitulating the history of mathematics by having the automated theorem prover generate lemmas , right ?

And its lemmas will induce a certain curvature of , of matta mathematical space .

Mhm So in other words , to every , it's like a machine that's laying out masses in the universe , the um you know , it will induce a certain , you know , structured and mathematical meta mathematical space .

Um And uh OK , so that's what happens there .

So then in the actual , um so we , we can say in , in , in ordinary mathematics , you know , my , my long time project of curating the three million theorems of mathematics , we could imagine uh kind of , you know , if we had those , we could imagine their meta mathematical characteristics causing certain things to happen in the structure of G D six and so on in this meta mathematical space .

So , and , and so the consequence would be we can essentially , you know , we've effectively geometries the meta mathematics , which is what we were setting out to do .

And then OK , well , that's very cool .

I mean , I think I understand but the , so I think we understand what the analogy is between physics and mathematics .

Then , you know , in a sense , the layout of things in the physical world is analogous to the choice of axioms in the mathematical world .

Um Right .

And uh um I think um ok .

And so the thing we haven't discussed , you were about to make a point here .

What point were you about ?

Um So the , the , the set .

So I think we , I , I , I , I feel like we have a decent conceptual understanding now of some of this .

So the part that I don't , that I don't get , which is probably the part that Tuxes was here for and has been very patient is , is , is as we take this limit of rule space , what what , what is the road map for ?

What we will learn from that ?

Taking ?

What ?

Well , what I mean by that is OK .

So when we take this limit of going to rural space , we the sort of the the we're defining the maximally nonn free mathematical structure indeed .

Right .

Indeed .

And what on earth does that mean ?

And then the claim would be , yeah , that , that all the mathematical structures can be constructed by foliation or by vibration of that , right , which is to say that that contains , you know , in the Hilbert program kind of way that contains all the ultimate statements of sort of that contains all the all the statements of ultimate limiting mathematics .

But the mathematics that we find interesting might be much freer than that .

Right .

Right .

And may not be in , you know , in the , in the case of non constructivism may not be attainable by any finite completion procedure applied to the multi way system , right ?

But so that is the limiting , that's the limit of mathematics as , as we put more and more constraints on .

So why is the limit ?

OK .

So the one thing that's sort of interesting is the limit of mathematics as we put more mathematical constraints seems to converge with the limit of physics .

I see .

So , so the point there is it doesn't matter all the mathematical efforts that we put in all the efforts to understand the physical universe that we have both eventually converge to the same thing which is again , the statement , everything is computational .

That's in the end what ?

That's all that's really saying , but this is giving a more mathematical structure to that limit point .

I mean , it's the limit point to both both there , there's the limit point .

Yes , we can see that's the actual , there's a limit point , right ?

Um More extreme one .

Yes .

Right .

So that that's the limit point of and the significance of that limit point .

So if we think about this , in analogy with statistical mechanics , if this is the renewal organization group fixed point , the question is there's a whole relevant and irrelevant operators story associated with what you know , as you add in as you , as you consider things which , which basically limit out at the fixed point versus things that are still rattling around .

That is saying , I think that's like the vibration story .

Mhm hm .

Very interesting .

Ok , this , this , I'm , I'm sorry , we , we've gone off on this .

Ok , I think we , we are more or less done with the , with this particular track .

So , so now we , now we really can do the , the , the rule but , but I mean , just any , any thoughts on sort of the road map of what we will achieve by thinking about the ral fixed point basically , or the rule limit , what might we achieve from that does maybe Xerxes has an opinion if , if we didn't , if we didn't , we didn't lose him .

Yes .

You mean uh for , for , for mathematics or for physics ?

For either one , either one , I mean , what , what do we learn from seeing the this limiting ?

I mean , you know , in computer science there is extreme nondeterminism that is the graph in mathematics , it's extreme relations , so to speak .

Yeah .

What are we gonna say ?

So can , can expand on this , I'm sure .

But for me , the most interesting thing that so far about the Ral space both in physics and in mathematics is the , is the fact that it endows everything with , with geometry , right ?

It's the thing that explains why we have , you know , Hilbert spaces and spacetime and Rieman , you know , uh Romanian manifolds and things in physics .

And it explains why we have , it explains why lead groups have differential manifold structure and why , you know , topological groups have topological space structure and all that kind of stuff .

It's right .

It's because it's inheriting the spatial structure from the , from the Ral group .

Yeah .

No , no , that's interesting .

I mean , so that , that is , so the analogy in statistical physics would be something like um gosh , I think there's an analogy in both statistical physics and things like conformal field theory and so on .

Um I completely know what it is but , but , but because the fixed point has certain properties , you're saying that even when we do not reach the fixed point , we still have , you know , a bunch of those properties .

And , and the understanding which I don't yet have , which maybe you can explain a different time is why does the structure of the rural space ?

What is this growth and des hypothesis or is this approved fact that the infinity group oid has this geometrical structure or topological structure ?

This is growth and dee hypothesis .

But again , please , please please chime in but no .

So , so , so that's correct that that is growth in the hypothesis .

But what's uh what's maybe interesting here is that this uh this root real multi way uh system is giving a very concrete realization of these uh infinity uh topos .

And in , in such a way that uh in , in , in , in , by using this structure , one can nicely realize all the all the universal constructions on on this topos that realize physics as well as realize mathematics but maybe perhaps goes could go a little bit further than what is usually done in the in the program of realizing physics and mathematics .

Because most of the time when people are talking about realizing physics or mathematics , they are talking either about observable uh physics or probable mathematics .

But in some sense , while this rural monkey way system is , is really uh a kind of nice , uh let's say calculus of infinity to it .

Kind of gives us some more insights into what type of physics and mathematics might lie perhaps outside of uh standard observation or probability in the sense that if you , if , if you think about all , all the pos uh if you think about the rule and multi system as some sort of cellular automata , they themselves realize certain classifications .

So I would say that a section of the rules that , that give you physics as you observe in the world would look like automata of class four .

Whereas there might be some type of rules in the , in the , in the tower of infinity tower of uh uh of the , of the space that might realize a multi way system that is more like rule 30 .

And , and that might be that might give rise to universes or physics or mathematics that is unlike anything of what you observe here , it's still part of the infinity to , but it is giving you some different type of uh physics and mathematics .

At least not the type that we are used to in terms of constructing And so the question , this is the alien intelligences question .

This is the question of , is there a slice of the ral multi way system that is the slice that , you know , can we imagine the alien intelligence basically ?

And what , what you're saying is this rule multi way system encodes everything any alien intelligence could , could view the universe to be .

Yeah , it has to because the , the way we've constructed this rural multi way system is that we have , we have really purposely thought of it as something that has not only rules but rules of rules and rules of rules to to up to an infinite tower .

So in all the in this entire to there has to be something like a rule 30 at least one such case has to exist .

And , and if you , if you look at just that section and , and look at the multi wave fibers coming from that section , it has to realize something of an of an alien type , quote unquote alien type .

No , no , I agree .

I agree .

But , but so another way to look at this would be , you know , we can think of languages for describing the world and just like , you know , we have universal algebra and so on as a way to in mathematics .

OK .

So , so think about it mathematically think , you know , forget the physics case for a second , just think about it mathematically , you know , we have a sort of a tower of mathematics that lives on top of things like universal algebra .

So , a question would be , is there an utterly different , you know , complications for aliens ?

Good , good , good topic .

Um Yeah .

Right .

More general than universal algebra .

Yes .

Well , right .

But the whole point is , is there an alternative universal algebra is one language for talking about , um , you know , axiomatic systems ?

But there could , you know what the point being made here is that can be completely different .

So the question is , what could we imagine that isn't universal algebra as a and have mathematicians even invented things that are not things like universal algebra .

I mean , when people write down axiomatic systems , are they always doing it ?

And uh go ahead uh there , there , there is just so since you asked if there are , there are mathematicians thinking about that , that there is just one kind of controversial example of this recent uh uh recent so-called proof of the ABC conjecture where uh uh Mozuki tried to come up with what , what , what I think he calls inter universal algebra .

It's claimed to be more general .

But currently , it's highly controversial and it's not uh if it is true , then it is uh trying to be a system that generalize it goes even more general than universal algebra .

I think he calls it inter inter universal algebra or inter universal type Mueller theory , something like inter universal type Mueller theory .

Yeah .

In , in , in that the uh he , he , they , they try to prove many things .

Be beyond , beyond even the ABC conjecture .

So , what is it ?

So , is it , is it a ?

Wow .

OK .

So it's so , so all I can say now , I mean , uh , I mean , there are very few people in the world who understand that .

I'm certainly not one of them but , but uh he , he , they try to , they try to even define uh the most basic operations of multiplication .

They try to do everything even more at generally than , than what universal algebra could possibly lay down .

OK .

But so in the context of the specifics of the things like the ABC conjecture .

So , I mean , he hasn't , has he tried to do it in , I mean , this is I'm looking at some stuff here .

I mean , this starts with the , the most basic thing here is an elliptic curve and that's blah blah blah blah blah with elliptic curves .

Um But my question is , I mean , universal algebra is very , very simple to define .

So does , does he have a definition of this ?

That is something ?

Um Is that right ?

Is that what it does ?

Yeah .

So , so I , I , I don't know the answer to that and uh um I don't know the exact answer to that , but I'm also not sure if the system that he has built up can actually be verified with , with the way we use current mathematics .

I don't know if the current probably a different axiomatic system .

Yeah .

Yeah .

Right .

So it's just like , so is it the case just to understand the structure of this ?

I mean , we have set theory , we have , you know , universal foundations .

Do they prove the same set of things ?

Presumably not ?

No , I don't think so .

So what's an example of something that can be proved by one but not by the other which anybody cares about ?

Because this is the , you know , this is another long running thing of mine is , you know , what's , what's the simplest undecidable diph equation ?

But alternatively said , given a , um uh you know , for any given axiomatic system in mathematics , I mean , it's a little bit weird for me to even say that .

But , but I guess , you know , is OK , not naive question if , if we make the proof of Fermat's last theorem , for example , which we don't know exactly what the axiomatic system that it depends on is maybe it's piano arithmetic plus set theory .

But who knows ?

Could we imagine two different competing proofs ?

One of which is based on un foundations and one of which is based on set theory and could they even come to different conclusions ?

I mean , could one of them say Fermat's last theorem ?

Well , one of them might say it's provable and one of them might say it's not provable , isn't that correct ?

Yeah , I mean , it's hard to see how it would work for F L T but for , you know , in general , because valent foundations are uh you know , constructive and set theory is non constructive .

It's , it's easy to see how you could construct an example of such a theorem .

Do you know if people have them ?

I mean , so , so , but in other words , look in , I mean , what all we're saying is the aliens have can have completely different , you know , where , where was that ?

A mega example ?

I thought that was a nice example .

Well , this was the omega example for , for finding digits of omega an infinite set of , of um there was a particular , that's something that is conceivably provable in set theory but is not conceivably provable in any constructive system .

Yes , by the way , I mean , Greg chain has often talked about weighing axioms as in what is the , you know , in the , in the context of algorithmic information theory .

There is a notion of weighing axioms which I don't think is quite the same as what we're describing here .

Yeah , we have .

That's right .

That that's the difference in his weighing of axioms .

It is basically there are no consequences to the axioms in , in his way of thinking about it in some sense .

Anyway , never mind .

I I I get that .

But , but um but but back to this .

So , so we're saying that there could be a completely different axiomatic system that might or might not look like our existing mathematics .

I mean , we could pick an axiomatic system .

I mean , just like I've just enumerated , you know , I spent effort enumerating random axiomatic systems .

So what is the difference between my , I mean , why has this um uh uh person , I mean , the claim would have to be , go ahead by the way , do you , do you mind if I just give a quick summary of kind of what the , what the basic idea of I E tech is , please .

So , so the um so the , the , the essential , you know , so , so the , the ABC conjecture , you know , the , the reason it's interesting is that , you know , it , it , it gives a nontrivial connection between addition and multiplication , right ?

That's kind of , that's , that's why it's interesting .

I mean , it's , it's the conjecture that , that A , that there exist .

Remind me what the actual thing is that if you take the radical of A times B times C and you raise it to the power of one plus epsilon that it , it , it's , it's a , it's a constraint on numbers of prime factors for , for , for um for sets of ABC that satisfy the equation A plus B for , for sets of integers A A B and C that satisfy A plus B equals C .

But anyway , the , the , the , the point is you start from an additive equation A plus B equals C and you derive a condition on a multiplicative relationship like the radical of A times B times C .

So it's giving you some relationship between addition multiplication .

So what I utech does , the idea is uh you , so you can define uh so , so suppose you have a , you know , a number field equipped with an elliptic curve which you can think of as being a , a universe , a a what a mathematical universe .

Mhm .

Now deform the ring structure .

Uh it would , it would specifically to form the multiplication operation for this ring structure to obtain a different , to obtain a deformed universe .

OK .

And then I utech gives you a way of computing , gives you an explicit algorithm actually for computing the resultant effect on the addition operation .

That's the basic idea using links between universes or between Hodge theaters .

He is the Hodge theater as they're called .

Well , this is part of the question uh within universes .

You know , the thing that makes me feel good about this is , is , is this for me , this kind of , you know , infinity group level mathematics has always seemed rather out of reach .

I think it , it's I I'm now , you know , it , it's a certain , sorry .

The reason why I bring this up is because I , I , I think I , you know , I , you is something that is kind of eminently relevant to , to the sort of stuff we're discussing here , right ?

Because it's basically saying , you know , you , you have a mathematical universe , you define an arithmetic on it .

Now you do , you , you , you very explicitly perform a defamation a a as you would do in ordinary , you know , type moler theory um which we can think of as being , you know , a geometrical def defamation , some kind of like cause like informal diamorphine or something .

Um And it affects one of the operations in this , you know , in this algebra .

What is the effect that it has on the other operations in the algebra ?

Um Yes , which I think is a , you know , when , when you start thinking about transformations between foliation of mathematical spaces and things that that's , that doesn't seem entirely relevant .

Um Well , for , for us , it is like taking a deformation in rural space , uh maybe even a kind of deformation uh by one of the infinity groups sitting there and then looking at a new multi way system from that resulting uh the the the new new fibers coming from that resulting deformation of rules , right ?

Oops the parameter of the effect of defamation , continuous defamation on real space one possible , but it's kind of crazy .

And who , who , who knows if I take a right .

Right .

Somebody is suggesting that we invite Greg chain .

Yes , I , I want Greg to come .

He keeps on saying that with his two young Children which who are remarkably young compared to him , he's his uh he has a computationally irreducible uh issue of of time slots and things .

Um the uh um but uh um actually he offered me an a , a speculation because I gave him like a few word summary of what we were doing .

And I'm actually going to look at what he said about because he said something kind of interesting , which he was assuming we were doing , which I think is not what we think we're doing , but it might be what we're actually doing .

Um , uh OK .

He's guessing it's a space of possible mathematical theories plus distance metric between theories .

Do we have a distance metric between theories ?

If , if we look at the geometry of the topos , then one could get a distance between theories .

Yeah .

Each theory is a rule fiber .

Yeah .

In , in , in some sense , what what we are sort of trying to do is there there is this uh the , the because this kind of links to the , what we spoke about the other day related to the Curry Harvard correspondence , there is actually a slight generalization of that already , which is called the Curry Harvard Lamber correspondence in which they link proofs programs and categories .

But what we are doing here is actually generalizing that one level further by , by linking proofs programs and infinity to and using , using these uh this tower of uh homotopia and infinity groups to generalize the Curry Howard Lambic .

So in , in , in , in that sense , in this , in this way of thinking uh this the , the rule of uh fibra gives us uh sit sitss where uh in , sits in the block where the infinity topos set .

And , and from that , you , you , we should be able to get all the possible uh types of calculus that people do in the Standard Curri Howard .

So the lambda calculus would be one realization as the car category , the Z Z Z calculus could be another realization as as a mono category in uh in the categorical quantum mechanics .

And more generally , the Homo toy algebras would be uh realizations of , of uh of uh Calculi that sit in the infinity topos coming or induced from uh induced from uh the , the uh these homotopia through the rural space .

So in , in that sense , we are generalizing mathematics uh by in fact , uh giving a generalization of a very concrete generalization of this uh correspondence .

Uh and , and the presentation of this as a rural multi way system that's very interesting .

I mean , OK .

Well , well , I mean , but , but so just so I understand that the , the sort of uh status of all these things , the growth and hypothesis of the connection between infinity group and an topology is , is still just a hypothesis .

Is that true ?

Well , I was gonna , I , this was something I was gonna mention earlier .

So in the context of homophobic type theory , gross hypothesis is taken as a definition , right , essentially that we use this as a way of defining what topology is .

So , yeah , I mean , you can claim it's a bit like the church turing thesis right , you can claim it's a hypothesis , but you can also claim it's a definition .

And in the , so in other words , this is , this is a , an outrageous , you know , like the statement , you know , you can define the number one as the , you know , the , the cardinality of the set of all sets that are not members of themselves or whatever .

This is a , you know , you can define basic topology in terms of this weird infinity , the properties of this weird infinity group .

Right .

Right .

Right .

Um Growth in the hypothesis has a definition of topology .

Topological spaces are infinity groups , but group os group .

S , yeah .

Oh , I'm glad we've got the spelling spelling system to know about groups now .

Um , oh , do we have ?

Oh , no , no way .

Um , I'll send it in .

Yeah , we , I'm , I'm a little disappointed that , uh , we don't , haven't had a packet update that causes to get updated as , as being , um , uh , spelling .

OK .

All right .

Listen , I , I should go , we've , we've , um , uh , we've come far in , um , in the weird world of meta mathematics .

Um , and , uh , yeah , and let's see , we heard a few comments on our live stream which we haven't completely gone through here .

Um , is it certain that you can't go faster than nonconstructive in proofs space ?

That's a good question .

Not if you want to maintain consistency with the proof network .

Well , non constructivism is just a statement that you're not constructive .

The question of whether there are hierarchies of non constructivism is a different question .

Um But , but going faster than non constructivism would be going fast , you know , be tipping beyond the light like path .

Sure .

I mean , so , so at that point , you're , you're , you're contradicting the partial order .

All right .

Um , I think we should wrap up here .

Um , so , well , thanks very much .

Thanks to people on the live stream and , um , we'll see you another time .